Module ProofState

module ProofState: sig .. end

The state of a proof, contains a set of active clauses (processed), a set of passive clauses (to be processed), and an ordering that is used for redundancy elimination.



module type S = ProofState_intf.S

Create a Proof State


module Make: 
functor (C : Clause.S) -> S with module C = C and module Ctx = C.Ctx