mc2 0.1 · OCaml Package

Core Library

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

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 Fmt = CCFormat

module Int_map : sig ... end

type level = int

Backtracking level

type ty_view = ..

Extensible view on types

type term_view = ..

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

type value_view = ..

Extensible view on values.

type lemma_view = ..

Extensible proof object

type 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

type tc_term

type class for terms, packing all operations on terms

type tc_value

type tc_lemma

type 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

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.

type 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 =

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

type actions

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

type 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

type 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

type var

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

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

type assignment_view =

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

type watch_res =

| Watch_keep
| Watch_remove

type premise_step =

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

type 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

package mc2

Core Library