module Make: functor (
C
:
Clause.S
) ->
S
with module C = C and module Ctx = C.Ctx
module Ctx: Ctx.S
module C: Clause.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 = (FOTerm.t * FOTerm.t * bool * C.t)
and type E.rhs = FOTerm.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