package mc2

  1. Overview
  2. Docs

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 =
  1. | Lemma_bool_tauto
    (*

    tautology a ∨ ¬a

    *)
  2. | 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 =
  1. | Bool
    (*

    Builtin type of booleans

    *)
  2. | Ty of {
    1. mutable id : int;
    2. view : ty_view;
    3. tc : tc_ty;
    }
    (*

    An atomic type, with some attached data

    *)

Types

type value =
  1. | V_true
  2. | V_false
  3. | 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 =
  1. | Eval_unknown
  2. | 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 =
  1. | A_bool of term * bool
  2. | A_semantic of term * value
type watch_res =
  1. | Watch_keep
  2. | Watch_remove
type premise_step =
  1. | Step_resolve of {
    1. c : clause;
    2. pivot : term;
    }
type check_res =
  1. | Sat
    (*

    The current set of assumptions is satisfiable.

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

Innovation. Community. Security.