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] |