package cvc5

  1. Overview
  2. Docs

Module Cvc5.SolverSource

Sourcetype solver
Sourceval mk_solver : ?logic:string -> TermManager.tm -> solver

Solver instance constructor.

Sourceval delete : solver -> unit

Solver instance destructor.

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

Assert a formula to the solver.

Parameters: - The formula to assert

Sourceval check_sat : solver -> Result.result

Check satisfiability.

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

Check satisfiability assuming a set of formulas.

Parameters: - The set of formulas to assume

Sourceval set_logic : solver -> string -> unit

Set the logic of the solver.

Sourceval set_option : solver -> string -> string -> unit

Set an option of the solver.

Parameters: - The option to set

  • The value of the option
Sourceval simplify : solver -> Term.term -> Term.term

Simplify a term or formula based on rewriting.

Sourceval push : solver -> int -> unit

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

Parameters: - The number of levels to push

Sourceval pop : solver -> int -> unit

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

Parameters: - The number of levels to pop

Sourceval reset : solver -> unit

Reset all assertions.

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval get_unsat_core : solver -> Term.term array

Get the unsatisfiable core.

Sourceval 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
Sourceval 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
Sourceval 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