package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

API

package libzipperposition

libzipperposition
- CHANGELOG
- README
- Library libzipperposition
  - Libzipperposition
    
    AC
    
    S
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    AC_intf
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    BBox
    
    Lit
    
    Set
    
    Tbl
    
    Bool_clause
    
    Bool_lit
    
    S
    
    PAYLOAD
    
    Make
    
    Set
    
    Tbl
    
    Bool_lit_intf
    
    S
    
    Set
    
    Tbl
    
    Classify_cst
    
    Clause
    
    S
    
    Make
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ClauseContext
    
    Set
    
    ClauseQueue
    
    S
    
    Make
    
    C
    
    WeightFun
    
    PriorityFun
    
    ClauseQueue_intf
    
    S
    
    C
    
    Ctx
    
    Lit
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    Clause_intf
    
    S
    
    Ctx
    
    Lit
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Const
    
    Cover_set
    
    Case
    
    Ctx
    
    S
    
    Key
    
    PARAMETERS
    
    Make
    
    Lit
    
    Ctx_intf
    
    S
    
    Lit
    
    Cut_form
    
    Pos
    
    Seq
    
    FV_tbl
    
    Env
    
    S
    
    Make
    
    Ctx
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Env_intf
    
    S
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Eprover_interface
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Make
    
    Env
    
    Extensions
    
    Ind_cst
    
    Cst_set
    
    Params
    
    ProofState
    
    S
    
    Make
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    ProofState_intf
    
    S
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Lit
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    SClause
    
    Sat_solver
    
    S
    
    Lit
    
    Make
    
    Lit
    
    Sat_solver_intf
    
    S
    
    Lit
    
    Saturate
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Make
    
    Env
    
    Selection
    
    Signals
    
    SimplM
    
    Infix
    
    Stream
    
    S
    
    ARG
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Make
    
    Ctx
    
    C
    
    StreamQueue
    
    S
    
    Make
    
    Stm
    
    WeightFun
    
    StreamQueue_intf
    
    S
    
    Stm
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    Stream_intf
    
    S
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Trail
    
    Lit
- Library libzipperposition.calculi
  - Libzipperposition_calculi
    
    App_encode
    
    T
    
    Arith_int
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Arith_rat
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Avatar
    
    S
    
    Make
    
    E
    
    Solver
    
    BLit
    
    Avatar_intf
    
    S
    
    E
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Solver
    
    Lit
    
    BLit
    
    Booleans
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    EnumTypes
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Fool
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Heuristics
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Higher_order
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    Ind_types
    
    Make
    
    Induction
    
    S
    
    Make
    
    Env
    
    Induction_intf
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Rewriting
    
    Make
    
    Simplex
    
    OrderedType
    
    S
    
    Make
    
    HELPER
    
    MakeHelp
    
    Superposition
    
    S
    
    Make
    
    Env
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Stm
    
    Ctx
    
    Lit
    
    C
    
    StmQ
    
    Stm
    
    WeightFun
    
    Superposition_intf
    
    S
    
    Env
    
    Ctx
    
    Lit
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    ProofState
    
    Ctx
    
    C
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    PS
    
    Ctx
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    CQueue
    
    C
    
    Ctx
    
    Tbl
    
    Seq
    
    Eligible
    
    ClauseSet
    
    Pos
    
    WithPos
    
    WeightFun
    
    PriorityFun
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    SubsumptionIndex
    
    C
    
    CLAUSE_SET
    
    ActiveSet
    
    SimplSet
    
    PassiveSet
    
    Stm
    
    Ctx
    
    Lit
    
    C
    
    StmQ
    
    Stm
    
    WeightFun
- Library libzipperposition.phases
  - Libzipperposition_phases
    
    Phases
    
    Infix
    
    Key
    
    Phases_impl
- Sources
  - libzipperposition
    
    AC.ml
    
    AC_intf.ml
    
    Bool_clause.ml
    
    Classify_cst.ml
    
    Cover_set.ml
    
    Cut_form.ml
    
    Ind_cst.ml
    
    SClause.ml
    
    bBox.ml
    
    bool_lit.ml
    
    bool_lit_intf.ml
    
    clause.ml
    
    clauseContext.ml
    
    clauseQueue.ml
    
    clauseQueue_intf.ml
    
    clause_intf.ml
    
    const.ml
    
    ctx.ml
    
    ctx_intf.ml
    
    env.ml
    
    env_intf.ml
    
    eprover_interface.ml
    
    extensions.ml
    
    libzipperposition.ml
    
    params.ml
    
    proofState.ml
    
    proofState_intf.ml
    
    sat_solver.ml
    
    sat_solver_intf.ml
    
    saturate.ml
    
    selection.ml
    
    signals.ml
    
    simplM.ml
    
    stream.ml
    
    streamQueue.ml
    
    streamQueue_intf.ml
    
    stream_intf.ml
    
    trail.ml
  - libzipperposition.calculi
    
    Arith_int.ml
    
    Arith_rat.ml
    
    Higher_order.ml
    
    Rewriting.ml
    
    app_encode.ml
    
    avatar.ml
    
    avatar_intf.ml
    
    booleans.ml
    
    enumTypes.ml
    
    fool.ml
    
    heuristics.ml
    
    ind_types.ml
    
    induction.ml
    
    induction_intf.ml
    
    libzipperposition_calculi.ml
    
    simplex.ml
    
    superposition.ml
    
    superposition_intf.ml
  - libzipperposition.phases
    
    libzipperposition_phases.ml
    
    libzipperposition_phases__.ml
    
    phases.ml
    
    phases_impl.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

libzipperposition

API

Library libzipperposition

Libzipperposition

Library libzipperposition.calculi

Libzipperposition_calculi

Library libzipperposition.phases

Libzipperposition_phases