module SMT:sig
..end
val benchmark_to_smtstring : context ->
string ->
string -> string -> string -> Expr.expr list -> Expr.expr -> string
val parse_smtlib_string : context ->
string ->
Symbol.symbol list ->
Sort.sort list ->
Symbol.symbol list -> FuncDecl.func_decl list -> unit
The symbol table of the parser can be initialized using the given sorts and declarations.
The symbols in the arrays in the third and fifth argument
don't need to match the names of the sorts and declarations in the arrays in the fourth
and sixth argument. This is a useful feature since we can use arbitrary names to
reference sorts and declarations.
val parse_smtlib_file : context ->
string ->
Symbol.symbol list ->
Sort.sort list ->
Symbol.symbol list -> FuncDecl.func_decl list -> unit
SMT.parse_smtlib_string
val get_num_smtlib_formulas : context -> int
ParseSMTLIBString
or ParseSMTLIBFile
.val get_smtlib_formulas : context -> Expr.expr list
ParseSMTLIBString
or ParseSMTLIBFile
.val get_num_smtlib_assumptions : context -> int
ParseSMTLIBString
or ParseSMTLIBFile
.val get_smtlib_assumptions : context -> Expr.expr list
ParseSMTLIBString
or ParseSMTLIBFile
.val get_num_smtlib_decls : context -> int
ParseSMTLIBString
or ParseSMTLIBFile
.val get_smtlib_decls : context -> FuncDecl.func_decl list
ParseSMTLIBString
or ParseSMTLIBFile
.val get_num_smtlib_sorts : context -> int
ParseSMTLIBString
or ParseSMTLIBFile
.val get_smtlib_sorts : context -> Sort.sort list
ParseSMTLIBString
or ParseSMTLIBFile
.val parse_smtlib2_string : context ->
string ->
Symbol.symbol list ->
Sort.sort list ->
Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
SMT.parse_smtlib_string
Returns A conjunction of assertions in the scope (up to push/pop) at the end of the string.
val parse_smtlib2_file : context ->
string ->
Symbol.symbol list ->
Sort.sort list ->
Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
SMT.parse_smtlib2_string