package cvc5

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type solver

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

val delete : solver -> unit

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

val check_sat : solver -> Result.result

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

val set_logic : solver -> string -> unit

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

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

val push : solver -> int -> unit

val pop : solver -> int -> unit

val reset : solver -> unit

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

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

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

val get_unsat_core : solver -> Term.term array

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

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

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