Module `Make.PS`

module Ctx = E.Ctx

module C = E.C

module CQueue = E.ProofState.CQueue: Priority queues on clauses

Useful Index structures

module TermIndex = E.ProofState.TermIndex

module UnitIndex = E.ProofState.UnitIndex

module SubsumptionIndex = E.ProofState.SubsumptionIndex

Common Interface for Sets

module type CLAUSE_SET = sig ... end

module ActiveSet = E.ProofState.ActiveSet

module SimplSet = E.ProofState.SimplSet

module PassiveSet = E.ProofState.PassiveSet

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