Mc2_core (p.mc2.0.1.doc.mc2.core.Mc2

Core Library

This library contains the core structures and algorithms of mc2. It defines terms, types, values, the main solver, plugins, etc.

Sourcemodule Atom : sig ... end

Sourcemodule Term : sig ... end

Sourcemodule Type : sig ... end

Sourcemodule Value : sig ... end

Sourcemodule Actions : sig ... end

Sourcemodule Builtins : sig ... end

Sourcemodule Clause : sig ... end

Sourcemodule Proof : sig ... end

Resolution proofs

Sourcemodule Solver : sig ... end

Main Interface for the Solver

Sourcemodule Service : sig ... end

Sourcemodule Plugin : sig ... end

Sourcemodule Tseitin : sig ... end

Tseitin CNF conversion

Sourcemodule ID : sig ... end

Sourcemodule Lemma : sig ... end

Sourcemodule Statement : sig ... end

Sourcemodule Bound_var : sig ... end

Sourcemodule Error : sig ... end

Sourcemodule Fmt = CCFormat

Sourcemodule Int_map = Util.Int_map

Sourcetype level = int

Backtracking level

Sourcetype ty_view = ..

Extensible view on types

Sourcetype term_view = ..

Extensible view on terms (generalized variables). Each plugin might declare its own terms.

Sourcetype value_view = ..

Extensible view on values.

Sourcetype lemma_view = ..

Extensible proof object

Sourcetype 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.)

Sourcetype tc_ty

Sourcetype tc_term

type class for terms, packing all operations on terms

Sourcetype tc_value

Sourcetype tc_lemma

Sourcetype 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.

Sourcetype 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 atom a which wraps f, while a.neg wraps the theory negation of f.

Sourcetype 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).

Sourcetype lemma =

| Lemma_bool_tauto
(*
tautology a ∨ ¬a
*)
| Lemma_custom of {
1. view : lemma_view;
  (*
  The lemma content
  *)
2. tc : tc_lemma;
  (*
  Methods on the lemma
  *)
}
(*
A lemma belonging to some plugin. Must be a tautology of the theory.
*)

Sourcetype actions

Actions available to terms/plugins when doing propagation/model building, including adding clauses, registering actions to do upon backtracking, etc.

Sourcetype ty =

| Bool
(*
Builtin type of booleans
*)
| Ty of {
1. mutable id : int;
2. view : ty_view;
3. tc : tc_ty;
}
(*
An atomic type, with some attached data
*)

Types

Sourcetype value =

| V_true
| V_false
| V_value of {
1. view : value_view;
2. 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

Sourcetype var

The "generalized variable" part of a term, containing the current assignment, watched literals/terms, etc.

Sourcetype 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 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)

Sourcetype assignment_view =

| A_bool of term * bool
| A_semantic of term * value

Sourcetype watch_res =

| Watch_keep
| Watch_remove

Sourcetype premise_step =

| Step_resolve of {
1. c : clause;
2. pivot : term;
}

Sourcetype 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

Sourcetype statement = Statement.t