package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Non-Perfect Discrimination Tree

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Map
  - Pos
  - Seq
  - Set
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFormula
  - FO
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Make
    
    Base
    
    Map
    
    MyT
    
    Seq
    
    Set
    
    TPTP
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Map
    
    From
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    To
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - S
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - TERM
    
    Seq
    
    Set
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Map
  - Pos
  - Seq
  - Set
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    H
    
    X
  - S
    
    H
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
    
    X
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
    
    X
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
    
    X
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Map
  - Pos
  - Seq
  - Set
  - Tbl
- LogtkSignature
  - SMap
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Map
  - Seq
  - Set
  - TPTP
    
    Arith
  - Tbl
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Map
  - Seq
  - Set
  - Subst
  - Tbl
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

Non-Perfect Discrimination Tree

This module provides a simplification index and a term index, based on a non-perfect discrimination tree (see "the handbook of automated reasoning", chapter "term indexing", for instance). It should be more compact in memory than LogtkDtree, and maybe more optimized too.

module Make (E : LogtkIndex.EQUATION) : LogtkIndex.UNIT_IDX with module E = E

module MakeTerm (X : Set.OrderedType) : LogtkIndex.TERM_IDX with type elt = X.t