A | |
| AC [FOTerm] | |
| AllocCache |
Simple Cache for Allocations
|
| Arith [Builtin] | |
| Arith [FOTerm] | |
| ArithOp [Builtin] | |
| Arr [AllocCache] | |
B | |
| BasicEquation [Index] | |
| Binder |
Binders
|
| Build [Position] | |
| Builtin |
Builtin Objects
|
C | |
| C [Index_intf.SUBSUMPTION_IDX] | |
| Classic [FOTerm] |
Classic view
|
| Cnf |
Reduction to CNF and simplifications
|
| Comparison |
Partial Ordering values
|
| Congruence |
Simple and Lightweight Congruence and order
|
| Constr [Precedence] |
Constraints
|
| Conv [Type] | |
| Conv [FOTerm] | |
| Ctx [TypeInference] | |
D | |
| DB [InnerTerm] | |
| DBEnv |
De Bruijn environments
|
| Default [Dtree] | |
| Dtree |
Perfect Discrimination Tree
|
E | |
| E [Index_intf.UNIT_IDX] |
Module that describes indexed equations
|
| Exn [Util] | |
F | |
| FO [Congruence] | |
| FO [Unif] | |
| FO [Substs] | |
| FOTerm |
First-order terms
|
| Feature [FeatureVector.Make] | |
| FeatureVector |
Feature Vector indexing
|
| Fingerprint |
Fingerprint term indexing
|
| Flag [Util] | |
| Form [TypedSTerm] | |
H | |
| HVar |
Hashconsed Variable
|
| Hashcons |
Hashconsing
|
I | |
| IArray |
Immutable Arrays
|
| ID |
Unique Identifiers
|
| IDOrBuiltin |
ID or Builtin
|
| Ind_ty |
Inductive Types
|
| Index |
Generic term indexing
|
| Index_intf |
Match the indexed terms against the given query term
|
| Inner [Unif] |
To be used only on terms without
InnerTerm.Multiset constructor
|
| InnerTerm |
Scoped Terms
|
| Interfaces |
Interfaces
|
L | |
| LazyList |
Lazy List
|
| Leaf [Index_intf.TERM_IDX] | |
| Loc [UntypedAST] | |
M | |
| Make [Multiset] | |
| Make [Hashcons] | |
| Make [FeatureVector] | |
| Make [Congruence] | |
| Make [NPDtree] | |
| Make [Fingerprint] | |
| Make [Dtree] | |
| MakeLeaf [Index] | |
| MakeNonWeak [Hashcons] |
Version that uses a regular Hashtbl, rather than a weak table.
|
| MakeTerm [NPDtree] | |
| Map [TypedSTerm] | |
| Map [ID] | |
| Map [Builtin] | |
| Map [STerm] | |
| Map [Type] | |
| Map [FOTerm] | |
| Map [InnerTerm] | |
| Multiset |
Generic multisets
|
| Multiset_intf |
Elements of the multiset
|
N | |
| NPDtree |
Non-Perfect Discrimination Tree
|
O | |
| Options |
Global CLI options
|
| Ordering |
Term Orderings
|
P | |
| ParseLocation |
Location in a file
|
| Pos [FOTerm] | |
| Pos [InnerTerm] | |
| Position |
Positions in terms, clauses...
|
| Precedence |
Precedence (total ordering) on symbols
|
R | |
| Renaming [Substs] | |
S | |
| SLiteral |
Simple Literal
|
| STerm |
S-like Terms.
|
| Scoped |
Scoped Value
|
| Section [Util] |
Debug section
|
| Seq [IArray] | |
| Seq [Multiset_intf.S] | |
| Seq [TypedSTerm] | |
| Seq [Precedence] | |
| Seq [Signature] | |
| Seq [STerm] | |
| Seq [Type] | |
| Seq [FOTerm] | |
| Seq [InnerTerm] | |
| Set [TypedSTerm] | |
| Set [ID] | |
| Set [Builtin] | |
| Set [Var] | |
| Set [STerm] | |
| Set [Type] | |
| Set [FOTerm] | |
| Set [InnerTerm] | |
| Signature |
Signature
|
| Skolem |
Skolem symbols
|
| Statement |
Statement
|
| StatementSrc |
Statement Source
|
| StringSet [STerm] | |
| Subst [TypedSTerm] | |
| Subst [Var] | |
| Substs |
Substitutions
|
T | |
| T [UntypedAST] | |
| TPTP [TypedSTerm] | |
| TPTP [Binder] | |
| TPTP [SLiteral] | |
| TPTP [Builtin] | |
| TPTP [STerm] | |
| TPTP [Type] | |
| TPTP [FOTerm] | |
| Tbl [TypedSTerm] | |
| Tbl [ID] | |
| Tbl [Builtin] | |
| Tbl [STerm] | |
| Tbl [Type] | |
| Tbl [FOTerm] | |
| Tbl [InnerTerm] | |
| Ty [TypedSTerm] | |
| Ty [Unif] | |
| Ty [Substs] | |
| TyBuiltin [TypeInference] | |
| Type |
Types
|
| TypeInference |
Type Inference
|
| TypedSTerm |
Simple Typed Terms.
|
U | |
| UStack [TypedSTerm] | |
| Unif |
Unification and Matching
|
| Unif_intf | bind subst v t binds v to t, but fails if v occurs in t
(performs an occur-check first)
|
| UntypedAST |
Main AST before Typing
|
| Util |
Some helpers
|
V | |
| Var |
Variable
|
| VarMap [Type] | |
| VarMap [FOTerm] | |
| VarMap [InnerTerm] | |
| VarSet [Type] | |
| VarSet [FOTerm] | |
| VarSet [InnerTerm] | |
| VarTbl [Type] | |
| VarTbl [FOTerm] | |
| VarTbl [InnerTerm] | |
Z | |
| ZF [TypedSTerm] | |
| ZF [Binder] | |
| ZF [SLiteral] | |
| ZF [Builtin] | |
| ZF [STerm] |