msat
Library
Module
Module type
Parameter
Class
Class type
type 'a printer = Format.formatter -> 'a -> unit
type ('term, 'form, 'value) sat_state = {
}
The type of values returned when the solver reaches a SAT state.
type ('atom, 'clause, 'proof) unsat_state = {
}
The type of values returned when the solver reaches an UNSAT state.
Export internal state
This type is used during the normalisation of formulas. See Expr_intf
.S.norm for more details.
type 'term eval_res =
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 neitherx
nory
are assigned to a valueValued (true, [x])
ifx
is assigned to0
Valued (true, [y])
ify
is assigned to0
Valued (false, [x; y])
ifx
andy
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 =
The type of reasons for propagations of a formula f
.
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. *) |
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 |
}
The type for a slice of assertions to assume/propagate in the theory.
type void = ( unit, bool ) gadt_eq
A provably empty type
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.