Module type Plugin_intf.S

module type S = sig .. end

Signature for theories to be given to the Model Constructing Solver.

type term

The type of terms. Should be compatible with Expr_intf.Term.t

type formula

The type of formulas. Should be compatble with Expr_intf.Formula.t

type proof

A custom type for the proofs of lemmas produced by the theory.

type level

The type for levels to allow backtracking.

val dummy : level

A dummy level.

val current_level : unit -> level

Return the current level of the theory (either the empty/beginning state, or the last level returned by the assume function).

val assume : (term, formula, proof)
       Plugin_intf.slice ->
       (formula, proof) Plugin_intf.res

Assume the formulas in the slice, possibly pushing new formulas to be propagated, and returns the result of the new assumptions.

val if_sat : (term, formula, proof)
       Plugin_intf.slice ->
       (formula, proof) Plugin_intf.res

Called at the end of the search in case a model has been found. If no new clause is pushed and the function returns Sat, then proof search ends and 'sat' is returned, else search is resumed.

val backtrack : level -> unit

Backtrack to the given level. After a call to backtrack l, the theory should be in the same state as when it returned the value l,

val assign : term -> term

Returns an assignment value for the given term.

val iter_assignable : (term -> unit) -> formula -> unit

An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms)

val eval : formula -> term Plugin_intf.eval_res

Returns the evaluation of the formula in the current assignment