Module Libzipperposition.ProofState

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