Module Msat.Solver_intf

Interface for Solvers

This modules defines the safe external interface for solvers. Solvers that implements this interface can be obtained using the Make functor in Solver or Mcsolver.

type 'a printer = Format.formatter -> 'a -> unit
type ('term, 'form, 'value) sat_state = {
eval : 'form -> bool;

Returns the valuation of a formula in the current state of the sat solver.

raises UndecidedLit

if the literal is not decided

eval_level : 'form -> bool * int;

Return the current assignement of the literals, as well as its decision level. If the level is 0, then it is necessary for the atom to have this value; otherwise it is due to choices that can potentially be backtracked.

raises UndecidedLit

if the literal is not decided

iter_trail : ('form -> unit) -> ('term -> unit) -> unit;

Iter thorugh the formulas and terms in order of decision/propagation (starting from the first propagation, to the last propagation).

model : unit -> ('term * 'value) list;

Returns the model found if the formula is satisfiable.

}

The type of values returned when the solver reaches a SAT state.

type ('atom, 'clause, 'proof) unsat_state = {
unsat_conflict : unit -> 'clause;

Returns the unsat clause found at the toplevel

get_proof : unit -> 'proof;

returns a persistent proof of the empty clause from the Unsat result.

unsat_assumptions : unit -> 'atom list;

Subset of assumptions responsible for "unsat"

}

The type of values returned when the solver reaches an UNSAT state.

type 'clause export = {
hyps : 'clause Vec.t;
history : 'clause Vec.t;
}

Export internal state

type negated =
| Negated

changed sign

| Same_sign

kept sign

This type is used during the normalisation of formulas. See Expr_intf.S.norm for more details.

type 'term eval_res =
| Unknown

The given formula does not have an evaluation

| Valued of bool * 'term list

The given formula can be evaluated to the given bool. The list of terms to give is the list of terms that were effectively used for the evaluation.

The type of evaluation results for a given formula. For instance, let's suppose we want to evaluate the formula x * y = 0, the following result are correct:

  • Unknown if neither x nor y are assigned to a value
  • Valued (true, [x]) if x is assigned to 0
  • Valued (true, [y]) if y is assigned to 0
  • Valued (false, [x; y]) if x and y are assigned to 1 (or any non-zero number)
type ('term, 'formula, 'value) assumption =
| Lit of 'formula

The given formula is asserted true by the solver

| Assign of 'term * 'value

The term is assigned to the value

Asusmptions made by the core SAT solver.

type ('term, 'formula, 'proof) reason =
| Eval of 'term list

The formula can be evalutaed using the terms in the list

| Consequence of unit -> 'formula list * 'proof

Consequence (l, p) means that the formulas in l imply the propagated formula f. The proof should be a proof of the clause "l implies f".

invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.

note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.

The type of reasons for propagations of a formula f.

type lbool =
| L_true
| L_false
| L_undefined

Valuation of an atom

type ('term, 'formula, 'value, 'proof) acts = {
acts_iter_assumptions : (('term, 'formula, 'value) assumption -> unit) -> unit;

Traverse the new assumptions on the boolean trail.

acts_eval_lit : 'formula -> lbool;

Obtain current value of the given literal

acts_mk_lit : 'formula -> unit;

Map the given formula to a literal, which will be decided by the SAT solver.

acts_mk_term : 'term -> unit;

Map the given term (and its subterms) to decision variables, for the MCSAT solver to decide.

acts_add_clause : ?⁠keep:bool -> 'formula list -> 'proof -> unit;

Add a clause to the solver.

parameter keep

if true, the clause will be kept by the solver. Otherwise the solver is allowed to GC the clause and propose this partial model again.

acts_raise_conflict : b. 'formula list -> 'proof -> 'b;

Raise a conflict, yielding control back to the solver. The list of atoms must be a valid theory lemma that is false in the current trail.

acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;

Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of eval_res

}

The type for a slice of assertions to assume/propagate in the theory.

type ('a, 'b) gadt_eq =
| GADT_EQ : ('a, 'a) gadt_eq
type void = (unit, bool) gadt_eq

A provably empty type

exception No_proof
module type FORMULA = sig ... end
module type EXPR = sig ... end

Formulas and Terms required for mcSAT

module type PLUGIN_CDCL_T = sig ... end

Signature for theories to be given to the CDCL(T) solver

module type PLUGIN_MCSAT = sig ... end

Signature for theories to be given to the Model Constructing Solver.

module type PLUGIN_SAT = sig ... end

Signature for pure SAT solvers

module type PROOF = sig ... end
module type S = sig ... end

The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.