Previous  Up  Next

Module Theory_intf

module Theory_intf: sig .. end

SMT Theory

This module defines what a theory must implement in order to be used in an SMT solver.

type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res =
| Sat (*

The current set of assumptions is satisfiable.

*)
| Unsat of 'formula list * 'proof (*

The current set of assumptions is *NOT* satisfiable, and here is a theory tautology (with its proof), for which every litteral is false under the current assumptions.

*)

Type returned by the theory. Formulas in the unsat clause must come from the current set of assumptions, i.e must have been encountered in a slice.

type ('form, 'proof) slice = {
   start : int; (*

Start of the slice

*)
   length : int; (*

Length of the slice

*)
   get : int -> 'form; (*

Accesor for the formuals in the slice. Should only be called on integers i s.t. start <= i < start + length

*)
   push : 'form list -> 'proof -> unit; (*

Allows to add to the solver a clause.

*)
   propagate : 'form -> 'form list -> 'proof -> unit; (*

propagate lit causes proof informs the solver to propagate lit, with the reason that the clause causes => lit is a theory tautology. It is faster than pushing the associated clause but the clause will not be remembered by the sat solver, i.e it will not be used by the solver to do boolean propagation.

*)
}

The type for a slice. Slices are some kind of view of the current propagation queue. They allow to look at the propagated literals, and to add new clauses to the solver.

module type S = sig .. end