The type of solvers.

The type of underlying solver instances.

solver_time tracks the time spent inside the SMT solver.

solver_count tracks the number of queries made to the SMT solver.

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

create ?params ?logic () creates a new solver.

• ?params is of type Params.t and is used to modify/set parameters inside the solver.
• ?logic is of type Logic.t and is used to set the theory of the assertions used. When the underlying theory is known, setting this parameter can improve solver performance. The default logic is ALL.

interrupt solver interrupts the current solver operation.

clone solver creates a copy of the solver solver.

push solver creates a backtracking point in the solver solver.

pop solver n backtracks n backtracking points in the solver solver.

reset solver resets the solver solver, removing all assertions.

add solver exprs asserts one or multiple constraints exprs into the solver solver.

add_set solver set asserts constraints from the set set into the solver solver.

get_assertions solver retrieves the set of assertions in the solver solver.

• deprecated Please use 'get_statistics' instead

get_statistics solver retrieves statistics from the solver solver.

check solver es checks the satisfiability of the assertions in the solver solver using the assumptions in es. Returns `Sat, `Unsat, or `Unknown.

check_set solver set checks the satisfiability of the assertions in the solver solver using the assumptions in the set set. Returns `Sat, `Unsat, or `Unknown.

get_value solver expr retrieves an expression denoting the model value of the given expression expr. Requires that the last check query returned `Sat.

model ?symbols solver retrieves the model of the last check query. If ?symbols is provided, only the values of the specified symbols are included. Returns None if check was not invoked before or its result was not `Sat.

Not compatible with cached solver mode - use get_sat_model instead

• see get_sat_model

  For cached solver-compatible alternative

Compute and retrieve a model for specific constraints.

get_sat_model ?symbols solver exprs performs: 1. check_set with exprs constraints 2. Returns model if result is `Sat

Filters output using ?symbols when provided. Designed for cached solvers.

• see model

  For non-cached solvers when you have already performed your own check/check_set and want to retrieve the results