package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Useful Index structures
Common Interface for Sets
Misc

libzipperposition
- Libzipperposition
  - AC
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - AC_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - BBox
    
    Lit
    
    Set
    
    Tbl
  - Bool_clause
  - Bool_lit
    
    Make
    
    Payload
    
    Set
    
    Tbl
    
    PAYLOAD
  - Bool_lit_intf
    
    S
    
    Set
    
    Tbl
  - Classify_cst
  - Clause
    
    Make
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
  - ClauseContext
    
    Set
  - ClauseQueue
    
    Make
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    PriorityFun
    
    WeightFun
  - ClauseQueue_intf
    
    S
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    PriorityFun
    
    WeightFun
  - Clause_intf
    
    S
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
  - Combinators
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Combinators_base
  - Const
  - Cover_set
    
    Case
  - Ctx
    
    Key
    
    Make
    
    Lit
    
    X
    
    PARAMETERS
  - Ctx_intf
    
    S
    
    Lit
  - Cut_form
    
    FV_tbl
    
    X
    
    Pos
    
    Seq
  - Env
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    X
    
    Ctx
    
    Lit
  - Env_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Eprover_interface
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Extensions
  - Ind_cst
    
    Cst_set
  - Lift_lambdas
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Params
  - ProofState
    
    Make
    
    ActiveSet
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - ProofState_intf
    
    S
    
    ActiveSet
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    Ctx
    
    Lit
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - SClause
  - Sat_solver
    
    Make
    
    S
  - Sat_solver_intf
    
    S
  - Saturate
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Selection
  - Signals
  - SimplM
    
    Infix
  - Stream
    
    ARG
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    Make
    
    A
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
  - StreamQueue
    
    ARG
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    Make
    
    A
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    WeightFun
  - StreamQueue_intf
    
    S
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    WeightFun
  - Stream_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
  - Trail
libzipperposition.avatar
- Libzipperposition_avatar
  - Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Sat
  - S
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Solver
  - UnionFind
    
    Make
    
    P
    
    PAIR
libzipperposition.calculi
- Libzipperposition_calculi
  - App_encode
  - Bce
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Bce_pe_fixpoint
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Bool_encode
  - Booleans
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - EnumTypes
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Eq_encode
  - Fool
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Heuristics
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Higher_order
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Hlt_elim
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Ind_types
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Lazy_cnf
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Pred_elim
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Pure_literal_elim
    
    IDMap
  - Rewriting
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Superposition
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    C
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Superposition_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    C
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
libzipperposition.induction
- Libzipperposition_induction
  - Make
    
    A
    
    Solver
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
libzipperposition.phases
- Libzipperposition_phases
  - Phases
    
    Infix
    
    Key
  - Phases_impl

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Ctx = Ctx

module C = C

module CQueue : ClauseQueue.S with module C = C and type C.t = C.t

Priority queues on clauses

Useful Index structures

module TermIndex : Logtk.Index.TERM_IDX with type elt = C.WithPos.t

module UnitIndex : 
  Logtk.Index.UNIT_IDX
    with type E.t = Logtk.Term.t * Logtk.Term.t * bool * C.t
     and type E.rhs = Logtk.Term.t

module SubsumptionIndex : Logtk.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