View Source cure_smt_parser (cure v0.1.0)

Cure SMT Model Parser

Parses S-expression output from SMT solvers (Z3, CVC5) to extract variable bindings and convert them to Erlang terms.

Features

  • Parse (model ...) sections
  • Extract (define-fun ...) statements
  • Convert SMT values to Erlang terms
  • Handle Int, Bool, Real types
  • Error handling for malformed output

Usage 

% Parse model from Z3 output
Lines = [
    <<\"(\">>,
    <<\"  (define-fun x () Int 5)\">>,
    <<\"  (define-fun y () Int 3)\">>,
    <<\")\">>
],
{ok, Model} = cure_smt_parser:parse_model(Lines).
% => {ok, #{x => 5, y => 3}}

Summary

Functions

extract_bindings(ModelText)

Extract variable bindings from model text.

parse_define_fun(Line)

Parse a (define-fun ...) statement.

parse_model/1

Parse a model from solver output lines.

parse_value(ValueBin)

Parse a value without type information.

parse_value/2

Parse a value based on its SMT type.

Functions

extract_bindings(ModelText)

-spec extract_bindings(binary()) -> [{atom(), term()}].

Extract variable bindings from model text.

Finds all (define-fun ...) statements and extracts variable bindings.

Arguments

  • ModelText - Binary containing model S-expressions

Returns

  • List of {Name, Value} tuples

parse_define_fun(Line)

-spec parse_define_fun(binary()) -> {ok, {atom(), term()}} | {error, term()}.

Parse a (define-fun ...) statement.

Extracts variable name, type, and value from a define-fun statement.

Arguments

  • Line - Binary line containing define-fun

Returns

  • {ok, {Name, Value}} - Parsed binding
  • {error, Reason} - Parse error

parse_model/1

-spec parse_model([binary()]) -> {ok, map()} | {error, term()}.

Parse a model from solver output lines.

Takes a list of binary lines from the solver and extracts variable bindings.

Arguments

  • Lines - List of binary lines from solver output

Returns

  • {ok, Model} - Map of variable names to values
  • {error, Reason} - Parse error

Example 

Lines = [<<\"(\">>, <<\"  (define-fun x () Int 5)\">>, <<\")\">>],
{ok, #{x => 5}} = parse_model(Lines).

parse_value(ValueBin)

-spec parse_value(binary()) -> term().

Parse a value without type information.

Attempts to infer type and parse accordingly.

Arguments

  • ValueBin - Binary containing the value

Returns

  • Erlang term (guessed type)

parse_value/2

-spec parse_value(atom(), binary()) -> term().

Parse a value based on its SMT type.

Converts SMT-LIB value representation to Erlang term.

Arguments

  • Type - SMT type atom ('Int', 'Bool', 'Real')
  • ValueBin - Binary containing the value

Returns

  • Erlang term (integer, boolean, float)