Module type SolverSig.Inst

module type Inst = sig .. end
Sigature of a solver instance

module Conv: SMTExpr.Conv 
val delete_instance : unit -> unit
Delete and stops the instance of the solver

Declarations


val declare_sort : SMTExpr.sort -> SolverResponse.decl_response
Declare a new sort symbol
val declare_fun : string -> SMTExpr.sort list -> SMTExpr.sort -> SolverResponse.decl_response
Declare a new function symbol
val define_fun : string ->
SMTExpr.var list -> SMTExpr.sort -> SMTExpr.t -> SolverResponse.decl_response
Define a new function symbol as an abbreviation for an expression

Commands


val assert_expr : SMTExpr.t -> SolverResponse.decl_response
Assert the expression
val push : int -> SolverResponse.decl_response
Push a number of empty assertion sets to the stack
val pop : int -> SolverResponse.decl_response
Pop a number of assertion sets from the stack
val check_sat : ?timeout:int -> unit -> SolverResponse.check_sat_response
Check satisfiability of the asserted expressions

The optional parameter timeout limits the maximum runtime to the given number of milliseconds

val check_sat_assuming : SMTExpr.t list -> SolverResponse.check_sat_response
Check satisfiability of the asserted expressions assuming the input literals.
val check_sat_assuming_supported : unit -> bool
Indicates whether the solver supports the check-sat-assuming command.
val get_value : SMTExpr.t list -> SolverResponse.get_value_response
Get the assigned values of expressions in the current model
val get_model : unit -> SolverResponse.get_model_response
Get the assigned values of expressions in the current model
val get_unsat_core : unit -> SolverResponse.get_unsat_core_response
Get an unsatisfiable core of named expressions
val execute_custom_command : string -> SMTExpr.custom_arg list -> int -> SolverResponse.custom_response
Execute a custom command and return its result

execute_custom_command s c a r sends a custom command s with the arguments a to the solver instance s. The command expects r S-expressions as result in case of success and returns a pair of the success response and a list of S-expressions.

val execute_custom_check_sat_command : string -> SolverResponse.check_sat_response
val trace_comment : string -> unit