Module Libzipperposition.ProofStateSource

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.

Sourcemodule type S = ProofState_intf.S

Create a Proof State

Sourcemodule Make (C : Clause.S) : S with module C = C and module Ctx = C.Ctx