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.

val get_units : solver -> Expr.expr list

Retrieve the set of units from the solver. Units are clauses of size 1 learned by the solver during solving.

val get_non_units : solver -> Expr.expr list

Retrieve the set of non-units from the solver. Non-units are clauses of size greater than 1 learned by the solver.

val get_trail : solver -> Expr.expr list

Retrieve the trail (sequence of assignments) from the solver. The trail shows the sequence of literal assignments made by the solver.

val get_levels : solver -> Expr.expr list -> int array

Retrieve the decision levels of trail literals. Given a list of literals from the trail, returns an array of their decision levels.

Returns Array of decision levels corresponding to the input literals

val congruence_root : solver -> Expr.expr -> Expr.expr

Retrieve the congruence closure root of an expression. Returns the representative of the equivalence class containing the expression.

val congruence_next : solver -> Expr.expr -> Expr.expr

Retrieve the next element in the congruence closure equivalence class. Congruence classes form a circular list; this returns the next element.

val congruence_explain : solver -> Expr.expr -> Expr.expr -> Expr.expr

Retrieve an explanation for why two expressions are congruent. Returns an expression that justifies the congruence between a and b.

val from_file : solver -> string -> unit

Parse SMT-LIB2 formulas from a file and assert them into the solver.

val from_string : solver -> string -> unit

Parse SMT-LIB2 formulas from a string and assert them into the solver.

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

Provide an initial value hint for a variable to the solver. This can help guide the solver to find solutions more efficiently.