msat 0.8 · OCaml Package

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 Msat__.Vec.t;
history : 'clause Msat__.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

formulas

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

Signature for a module handling proof by resolution from sat solving traces

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.

package msat