Functor Solver.DummyTheory

module DummyTheory: functor (F : Formula_intf.S) -> Theory_intf.S  with type formula = F.t
                 and type proof = F.proof

Simple case where the theory is empty and the proof type is the one given in the formula interface

Parameters:

F : Formula_intf.S

Signature for theories to be given to the Solver.

type formula

The type of formulas. Should be compatble with Formula_intf.S

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 : (formula, proof) Theory_intf.slice ->
       (formula, proof) Theory_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 : (formula, proof) Theory_intf.slice ->
       (formula, proof) Theory_intf.res

Called at the end of the search in case a model has been found. If no new clause is pushed, then '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,