package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Libraries

libzipperposition
- Libzipperposition
  - AC
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - AC_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - BBox
    
    Lit
    
    Set
    
    Tbl
  - Bool_clause
  - Bool_lit
    
    Make
    
    Payload
    
    Set
    
    Tbl
    
    PAYLOAD
  - Bool_lit_intf
    
    S
    
    Set
    
    Tbl
  - Bool_selection
  - 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
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - 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
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    X
    
    Ctx
    
    Lit
  - Env_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Eprover_interface
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Extensions
  - FormulaRename
    
    Make
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
  - Ind_cst
    
    Cst_set
  - Lift_lambdas
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - 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
    
    TPSet
  - Sat_solver
    
    Make
    
    S
  - Sat_solver_intf
    
    S
  - Saturate
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - 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
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    Make
    
    A
    
    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
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    Sat
  - S
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    Solver
  - UnionFind
    
    Make
    
    P
    
    PAIR
libzipperposition.calculi
- Libzipperposition_calculi
  - App_encode
  - Bce
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Bce_pe_fixpoint
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Bool_encode
  - Booleans
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos