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