cvc5 1.2.0 (latest) · OCaml Package

type solver

val mk_solver : ?logic:string -> TermManager.tm -> solver

Solver instance constructor.

val delete : solver -> unit

Solver instance destructor.

val assert_formula : solver -> Term.term -> unit

Assert a formula to the solver.

Parameters: - The formula to assert

val check_sat : solver -> Result.result

Check satisfiability.

val check_sat_assuming : solver -> Term.term array -> Result.result

Check satisfiability assuming a set of formulas.

Parameters: - The set of formulas to assume

val set_logic : solver -> string -> unit

Set the logic of the solver.

val set_option : solver -> string -> string -> unit

Set an option of the solver.

Parameters: - The option to set

The value of the option

val simplify : solver -> Term.term -> Term.term

Simplify a term or formula based on rewriting.

val push : solver -> int -> unit

Push (a) level(s) to the assertion stack.

Parameters: - The number of levels to push

val pop : solver -> int -> unit

Pop (a) level(s) from the assertion stack.

Parameters: - The number of levels to pop

val reset : solver -> unit

Reset all assertions.

val get_value : solver -> Term.term -> Term.term

Get the value of the given term in the current model.

Parameters: - The term for which the value is queried

val get_values : solver -> Term.term array -> Term.term array

Get the values of the given terms in the current model.

Parameters: - The terms for which the values is queried

val get_model_domain_elements : solver -> Sort.sort -> Term.term array

Get the domain elements of uninterpreted sort s in the current model. The current model interprets s as the finite sort whose domain elements are given in the return value of this function.

Parameters: - The uninterpreted sort in question

val get_unsat_core : solver -> Term.term array

Get the unsatisfiable core.

val get_model : solver -> Sort.sort array -> Term.term array -> string

Get the model.

Parameters: - The list of uninterpreted sorts that should be printed in the model

The list of free constants that should be printed in the model

val declare_fun : solver -> string -> Sort.sort array -> Sort.sort -> Term.term

Declare n-ary function symbol.

Parameters: - The name of the function

The sorts of the parameters of this function
the sort of the return value of this function

val define_fun : 
  solver ->
  string ->
  Term.term array ->
  Sort.sort ->
  Term.term ->
  Term.term

Define n-ary function.

Parameters: - The name of the function

The parameters of this function
The sort of the return value of this function
The function body

package cvc5