package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

LogtkPrecedence (total ordering) on symbols
1. LogtkSignature
2. Functor

package logtk

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

LogtkPrecedence (total ordering) on symbols

type symbol_status = LogtkPrecedence_intf.symbol_status =

| Multiset
| Lexicographic

LogtkSignature

module type S = LogtkPrecedence_intf.S

Functor

module type SYMBOL = sig ... end

module Make (Sym : SYMBOL) : S with type symbol = Sym.t

module Default : S with type symbol = LogtkSymbol.t

include module type of Default with type t = Default.t

type symbol = LogtkSymbol.t

type t = Default.t

Total LogtkOrdering on a finite number of symbols, plus a few more data (weight for KBO, status for RPC)

type precedence = t

val eq : t -> t -> bool

Check whether the two precedences are equal (same snapshot)

val snapshot : t -> symbol list

Current list of symbols, in decreasing order

val compare : t -> symbol -> symbol -> int

Compare two symbols using the precedence

val mem : t -> symbol -> bool

Is the symbol part of the precedence?

val status : t -> symbol -> LogtkPrecedence_intf.symbol_status

Status of the symbol

val weight : t -> symbol -> int

Weight of a symbol (for KBO). Strictly positive int.

val add_list : t -> symbol list -> t

Update the precedence with the given symbols

val add_seq : t -> symbol Sequence.t -> t

val declare_status : t -> symbol -> LogtkPrecedence_intf.symbol_status -> t

Change the status of the given precedence

module Seq : sig ... end

val pp_snapshot : Buffer.t -> symbol list -> unit

val pp_debug : Buffer.t -> t -> unit

val pp : Buffer.t -> t -> unit

val fmt : Format.formatter -> t -> unit

val to_string : t -> string

Builtin constraints

module Constr : sig ... end

type weight_fun = symbol -> int

val weight_modarity : arity:(symbol -> int) -> weight_fun

val weight_constant : weight_fun

val set_weight : t -> weight_fun -> t

Change the weight function of the precedence

since 0.5.3

Creation of a precedence from constraints

val create : ?weight:weight_fun -> Constr.t list -> symbol list -> t

make a precedence from the given constraints. Constraints near the head of the list are more important than constraints close to the tail. Only the very first constraint is assured to be totally satisfied if constraints do not agree with one another.

val create_sort : 
  ?weight:weight_fun ->
  (int * Constr.t) list ->
  symbol list ->
  t

Sort the list of constraints by increasing priority, then call create to build a precedence. The constraint with the smallest priority will be considered first.

since 0.6.1

val default : symbol list -> t

default precedence. Default status for symbols is Lexicographic.

val default_seq : symbol Sequence.t -> t

default precedence on the given sequence of symbols

val constr_list : t -> Constr.t list

Obtain the list of constraints

since 0.6.1

val with_constr_list : t -> Constr.t list -> t

Update the precedence by replacing its list of constraints. Caution, this can be dangerous (change the precedence totally, for instance)

since 0.6.1