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