• OCaml logo OCaml logo
  • Learn
  • Packages
  • Community
  • Blog
  • Playground
  • Searching...
    Or go to: Standard Library API
  • Learn
  • Packages
  • Community
  • Blog
  • Playground
  • Get started
  • libzipperposition

  • Documentation
  • libzipperposition.calculi lib
  • Libzipperposition_calculi .Simplex .Make Module
ON THIS PAGE
  • Parameters
  • Signature
    • Simplex construction
    • Simplex solving
    • Simplex optimizations
    • Access functions
    • Printing functions
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