Module Make.Solver

val make : ?params:Params.t -> ?logic:Logic.t -> unit -> solver

make ?params ?logic () creates a new solver with optional parameters params and logic logic.

val clone : solver -> solver

clone solver creates a copy of the solver solver.

val push : solver -> unit

push solver pushes a new context level onto the solver solver.

val pop : solver -> int -> unit

pop solver n pops n context levels from the solver solver.

val reset : solver -> unit

reset solver resets the solver solver to its initial state.

val add : ?ctx:term Symbol.Map.t -> solver -> term list -> unit

add solver ts adds the terms ts to the solver solver.

val check : ?ctx:term Symbol.Map.t -> solver -> assumptions:term list -> [ `Sat | `Unsat | `Unknown ]

check solver ~assumptions checks the satisfiability of the solver solver with the given assumptions. Returns `Sat, `Unsat, or `Unknown.

val model : solver -> model option

model solver retrieves the model from the solver solver, if one exists.

val add_simplifier : solver -> solver

add_simplifier solver adds a simplifier to the solver solver.

val interrupt : unit -> unit

interrupt () interrupts the current solver operation.

val get_statistics : solver -> Statistics.t

get_statistics solver retrieves statistics from the solver solver.

val pp_statistics : solver Fmt.t

pp_statistics fmt solver pretty-prints the statistics of the solver solver using the formatter fmt.