package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

The state of a proof, contains a set of active clauses (processed), a set of passive clauses (to be processed), and an ordering that is used for redundancy elimination.
1. Create a Proof State

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
    
    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
    
    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
    
    WeightFun
  - ClauseQueue_intf
    
    S
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    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
    
    Pos
    
    Seq
  - Env
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    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
    
    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
    
    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
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Selection
  - Signals
  - SimplM
    
    Infix
  - Trail
libzipperposition.calculi
- Libzipperposition_calculi
  - 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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Solver
  - 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
    
    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
    
    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
    
    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
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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
    
    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
    
    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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Induction
    
    Make
    
    A
    
    Solver
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Induction_intf
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Rewriting
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Simplex
    
    HELPER
    
    Make
    
    Var
    
    MakeHelp
    
    Var
    
    OrderedType
    
    S
  - 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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    C
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - 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
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    PS
    
    ActiveSet
    
    C
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    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

The state of a proof, contains a set of active clauses (processed), a set of passive clauses (to be processed), and an ordering that is used for redundancy elimination.

module type S = ProofState_intf.S

Create a Proof State

module Make (C : Clause.S) : S with module C = C and module Ctx = C.Ctx