libzipperposition 1.6 · OCaml Package

On This Page

Parameters
Signature

package libzipperposition

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
  - 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
  - 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
    
    Make
    
    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.calculi
- Libzipperposition_calculi
  - App_encode
  - Arith_int
    
    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
  - Arith_rat
    
    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
  - 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
  - Avatar_intf
    
    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
  - 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
  - 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
  - Ind_types
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet