Module Z3.Solver

module Solver: sig .. end

Solvers

type solver

type status =

`\|`	`UNSATISFIABLE`
`\|`	`UNKNOWN`
`\|`	`SATISFIABLE`

val string_of_status : status -> string

val get_help : solver -> string

A string that describes all available solver parameters.

val set_parameters : solver -> Params.params -> unit

Sets the solver parameters.

val get_param_descrs : solver -> Params.ParamDescrs.param_descrs

Retrieves parameter descriptions for solver.

val get_num_scopes : solver -> int

The current number of backtracking points (scopes). Solver.pop Solver.push

val push : solver -> unit

Creates a backtracking point. Solver.pop

val pop : solver -> int -> unit

Backtracks a number of backtracking points. Note that an exception is thrown if the integer is not smaller than Solver.get_num_scopes Solver.push

val reset : solver -> unit

Resets the Solver. This removes all assertions from the solver.

val add : solver -> Expr.expr list -> unit

Assert a constraint (or multiple) into the solver.

val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit

Assert multiple constraints (cs) into the solver, and track them (in the unsat) core using the Boolean constants in ps.

This API is an alternative to Solver.check with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using Solver.assert_and_track and the Boolean literals provided using Solver.check with assumptions.

val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit

Assert a constraint (c) into the solver, and track it (in the unsat) core using the Boolean constant p.

val get_num_assertions : solver -> int

The number of assertions in the solver.

val get_assertions : solver -> Expr.expr list

The set of asserted formulas.

val check : solver -> Expr.expr list -> status

Checks whether the assertions in the solver are consistent or not.

Model Solver.get_unsat_core Proof

val get_model : solver -> Model.model option

The model of the last Check.

The result is None if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

val get_proof : solver -> Expr.expr option

The proof of the last Check.

The result is null if Check was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled.

val get_unsat_core : solver -> Expr.expr list

The unsat core of the last Check.

The unsat core is a subset of Assertions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled.

val get_reason_unknown : solver -> string

A brief justification of why the last call to Check returned UNKNOWN.

val get_statistics : solver -> Statistics.statistics

Solver statistics.

val mk_solver : context -> Symbol.symbol option -> solver

Creates a new (incremental) solver.

This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

val mk_solver_s : context -> string -> solver

Creates a new (incremental) solver. Solver.mk_solver

val mk_simple_solver : context -> solver

Creates a new (incremental) solver.

val mk_solver_t : context -> Tactic.tactic -> solver

Creates a solver that is implemented using the given tactic.

The solver supports the commands Push and Pop, but it will always solve each check from scratch.

val add_simplifier : context ->
       solver -> Simplifier.simplifier -> solver

Create a solver with simplifying pre-processing *

val translate : solver -> context -> solver

Create a clone of the current solver with respect to a context.

val to_string : solver -> string

A string representation of the solver.

val interrupt : context -> solver -> unit

Solver local interrupt.

Normally you should use Z3_interrupt to cancel solvers because only one solver is enabled concurrently per context. However, per GitHub issue #1006, there are use cases where it is more convenient to cancel a specific solver. Solvers that are not selected for interrupts are left alone.