Functor ProofState.Make

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

module Ctx: Ctx.S 
module C: Clause_intf.S 
module CQueue: ClauseQueue.S  with module C = C and type C.t = C.t
Priority queues on clauses

Useful Index structures

module TermIndex: Index.TERM_IDX  with type elt = C.WithPos.t
module UnitIndex: Index.UNIT_IDX 
    with type E.t = (Term.t * Term.t * bool * C.t)
     and type E.rhs = Term.t
module SubsumptionIndex: Index.SUBSUMPTION_IDX  with type C.t = C.t

Common Interface for Sets

module type CLAUSE_SET = sig .. end
module ActiveSet: sig .. end
module SimplSet: CLAUSE_SET 
module PassiveSet: sig .. end

Misc

type stats = int * int * int 
statistics on the state (num active, num passive, num simplification)
val stats : unit -> stats
Compute statistics
val pp : unit CCFormat.printer
pretty print the content of the state
val debug : unit CCFormat.printer
debug functions: much more detailed printing