Module `YicesNative.Create`

The functor Create creates a new instance of the SMT solver with paramters passed as its arguments. The parameter argument P conataints a unique identifier id, initialized to the logic l and produces assignments if the optional labelled argument produce_assignments is true, proofs if produce_proofs is true and unsatisfiable cores if produce_cores is true.

Parameters

P : SolverSig.Params

Signature

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