libzipperposition

Library for Zipperposition
IN THIS PACKAGE

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 (C : Clause.S) : S with module C = C and module Ctx = C.Ctx