Module Mc2_core
Core Library
module Atom : sig ... end
module Term : sig ... end
module Type : sig ... end
module Value : sig ... end
module Actions : sig ... end
module Builtins : sig ... end
module Clause : sig ... end
module Proof : sig ... end
Resolution proofs
module Solver : sig ... end
Main Interface for the Solver
module Service : sig ... end
module Plugin : sig ... end
module Tseitin : sig ... end
Tseitin CNF conversion
module ID : sig ... end
module Lemma : sig ... end
module Statement : sig ... end
module Bound_var : sig ... end
module Error : sig ... end
module Int_map = Util.Int_map
type level
= Mc2_core__.Solver_types.level
Backtracking level
type ty_view
= Mc2_core__.Solver_types.ty_view
=
..
Extensible view on types
type term_view
= Mc2_core__.Solver_types.term_view
=
..
Extensible view on terms (generalized variables). Each plugin might declare its own terms.
type value_view
= Mc2_core__.Solver_types.value_view
=
..
Extensible view on values.
type lemma_view
= Mc2_core__.Solver_types.lemma_view
=
..
Extensible proof object
type decide_state
= Mc2_core__.Solver_types.decide_state
=
..
State carried by a given term, depending on its type, and used for decisions and propagations related to the term. Typically it contains a set of constraints on the values this term can have (lower/upper bounds, etc.)
type tc_ty
= Mc2_core__.Solver_types.tc_ty
type tc_term
= Mc2_core__.Solver_types.tc_term
type class for terms, packing all operations on terms
type tc_value
= Mc2_core__.Solver_types.tc_value
type tc_lemma
= Mc2_core__.Solver_types.tc_lemma
type term
= Mc2_core__.Solver_types.term
Main term representation. It is worth noting that terms are also (generalized) variables and behave mostly the same as boolean variables for the main solver, meaning that they need to be assigned a value in the model.
type atom
= Mc2_core__.Solver_types.atom
Atoms and variables wrap theory formulas. They exist in the form of triplet: a variable and two atoms. For a formula
f
in normal form, the variable v points to the positive atoma
which wrapsf
, whilea.neg
wraps the theory negation off
.
type clause
= Mc2_core__.Solver_types.clause
The type of clauses. Each clause generated should be true, i.e. enforced by the current problem (for more information, see the cpremise field).
type lemma
= Mc2_core__.Solver_types.lemma
=
|
Lemma_bool_tauto
tautology
a ∨ ¬a
|
Lemma_custom of
{
view : lemma_view;
The lemma content
tc : tc_lemma;
Methods on the lemma
}
A lemma belonging to some plugin. Must be a tautology of the theory.
type actions
= Mc2_core__.Solver_types.actions
Actions available to terms/plugins when doing propagation/model building, including adding clauses, registering actions to do upon backtracking, etc.
type ty
= Mc2_core__.Solver_types.ty
=
|
Bool
Builtin type of booleans
|
Ty of
{
mutable id : int;
view : ty_view;
tc : tc_ty;
}
An atomic type, with some attached data
Types
type value
= Mc2_core__.Solver_types.value
=
|
V_true
|
V_false
|
V_value of
{
view : value_view;
tc : tc_value;
}
A semantic value, part of the model's domain. For arithmetic, it would be a number; for arrays, a finite map + default value; etc. Note that terms map to values in the model but that values are not necessarily normal "terms" (i.e. generalized variables in the MCSat sense).
A value, either boolean or semantic
type var
= Mc2_core__.Solver_types.var
The "generalized variable" part of a term, containing the current assignment, watched literals/terms, etc.
type eval_res
= Mc2_core__.Solver_types.eval_res
=
|
Eval_unknown
|
Eval_into of value * term list
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 assignment_view
= Mc2_core__.Solver_types.assignment_view
=
|
A_bool of term * bool
|
A_semantic of term * value
type watch_res
= Mc2_core__.Solver_types.watch_res
=
|
Watch_keep
|
Watch_remove
type premise_step
= Mc2_core__.Solver_types.premise_step
=
|
Step_resolve of
{
c : clause;
pivot : term;
}
type check_res
= Mc2_core__.Solver_types.check_res
=
|
Sat
The current set of assumptions is satisfiable.
|
Unsat of atom list * lemma
The current set of assumptions is *NOT* satisfiable, and here is a theory tautology (with its proof), for which every literal is false under the current assumptions.
Result of checking satisfiability of a problem
type statement
= Statement.t