A | |
| A [Tip_lexer] | |
| A [Lex_kodkod] | |
| A [Parsing_utils] | |
| AnalyzeType |
Analyze Types : Cardinalities, Abstract, Incomplete
|
| Ast_kodkod |
Trivial AST for Kodkod models
|
B | |
| Binder [TermMono] | |
| Binder [TermInner] | |
| Builtin [TypeMono] | |
| Builtin [TypePoly] | |
| Builtin [Pattern] | |
| Builtin [TermMono] | |
| Builtin [TermInner] | |
| Builtin [FO] | |
| Builtin [UntypedAST] | |
C | |
| Callback [Utils] | |
| Cardinality |
Cardinalities
|
| Codata [ElimData] | |
| Conv [TPTP_model_ast] | |
| Conv [TermMono.TransFO] | |
| ConvBack [TermMono.TransFO] | |
| Convert [TypeInference] | |
| Convert [TermInner] | |
| Convert [Problem] |
Convert the term representations
|
D | |
| DT [Model] | |
| DT_util [Model] | |
| Data [ElimData] | |
| Decoder [Sexp_lib] | |
| Default [TermTyped] | |
| Default [TermInner] | |
| Default [Model] | |
E | |
| E [Parsing_utils] | |
| ElimCopy |
Eliminate Copy Types
|
| ElimData |
Encoding of Datatypes
|
| ElimIndPreds |
Eliminate Inductive Predicates
|
| ElimMultipleEqns |
Transform a problem with multiple equations per defined Symbol into one with single equations
|
| ElimPatternMatch |
Eliminate pattern-matching in Terms
|
| ElimRecursion |
Encoding of Recursive Functions
|
| ElimTypes |
Encoding of Simple Types
|
| Elim_HOF |
Elimination of Higher-Order Functions
|
| Elim_infinite |
Eliminate Infinite Types
|
| Elim_ite |
Eliminate "if/then/else"
|
| Elim_prop_args |
Eliminate function arguments of type "prop"
|
| Env |
Environment
|
| Erase [ID] |
Map to unique names
|
F | |
| FO |
First-Order Monomorphic Terms and Formulas
|
| FO_rel |
Relational FO Logic
|
| FO_tptp |
TPTP representation
|
| Features [Transform] | |
| FoToRelational |
FOL to Relational FO Logic
|
| Full [Reduce.Make] | |
| Fut [Scheduling] | |
I | |
| ID [TypeMono] | |
| ID [TermMono] | |
| ID |
Unique Identifiers
|
| Infix [Lazy_list] | |
| Intf |
Interfaces
|
| IntroGuards |
Introduce Guards
|
L | |
| LambdaLift |
Lambda Lifting
|
| Lazy_list |
Lazy List
|
| Lex_kodkod | |
| Lexer |
Lexer
|
| LiftRepr [TermTyped] | |
| Loc [Tip_lexer] | |
| Loc [Tip_ast] | |
| Loc [Parsing_utils] | |
| Loc [TermTyped] | |
| Loc [UntypedAST] | |
| Location |
Location in a file
|
M | |
| MVar [Scheduling] | |
| Make [TypeInference] | |
| Make [Parsing_utils] | |
| Make [TypeMono] | |
| Make [TypePoly] | |
| Make [Pattern] | |
| Make [TermMono] |
Build a representation and all the associated utilities
|
| Make [TypeCheck] | |
| Make [AnalyzeType] | |
| Make [Traversal] | |
| Make [Reduce] | |
| Make [TypeUnify] | |
| Map [TypeMono.S] |
A map on terms that only accepts terms
satisfying
is_ty as keys
|
| Map [TypeMono.Make] | |
| Map [TermInner.UTIL] |
Map with terms as key.
|
| Map [TermInner.Util] | |
| Map [ID] | |
| MetaVar [TypeMono] | |
| MetaVar |
Variables for Mutable Unification
|
| Model |
Model
|
| Model_clean |
Cleanup models
|
| Mono [TermMono.ToFO] | |
| Monomorphization |
Monomorphization
|
O | |
| OfFO [TermMono] | |
| Of_tptp [FO] | |
P | |
| P [TermMono.ToFO] | |
| P [TermInner.Default] | |
| Parse_kodkod | |
| Parse_tip |
Wrapper for TIP
|
| Parser | |
| Parsing_utils |
Various Utils for Parsing
|
| Pattern |
Pattern
|
| PerTbl [ID] | |
| Pipe [Transform] | |
| Polarity |
Polarity
|
| Polarize |
Polarize
|
| Prelude |
Prelude
|
| Print [TermTyped.Default] | |
| Print [TermInner] | |
| Print [Statement] | |
| Print [Env] | |
| Print [Problem] |
Printer for a problem
|
| Problem [FO] |
Problem
|
| Problem |
Top-Level Statements (with locations)
|
| ProblemMetadata |
Metadata attached to Problem
|
R | |
| Reduce |
Reductions, including Beta Reduction
|
| Res [Problem] | |
S | |
| Scheduling |
Scheduling of sub-processes
|
| Section [Utils] |
Debug section
|
| Set [Var] | |
| Set [ID] | |
| Sexp_lex | |
| Sexp_lib |
Simple and efficient S-expression parsing/printing
|
| Sig [TermMono] | |
| Signature |
Signature
|
| Skolem |
Skolemization
|
| Smbc_res [Tip_ast] | |
| Specialize |
Specialization
|
| Statement |
Top-level statement
|
| Subst [TypeMono] | |
| Subst [TermMono.ToFO] | |
| Subst [Var] | |
T | |
| T [TPTP_model_ast] | |
| T [TypeMono.S] | |
| T [TypeMono.Make] | |
| T [TypePoly.S] | |
| T [TypePoly.Make] | |
| T [Pattern.S] | |
| T [Pattern.Make] | |
| T [TermMono.S] | |
| T [TermMono.Make] | |
| T [FO] | |
| TI [TypeMono] | |
| TI [TypePoly] | |
| TI [Pattern] | |
| TI [TermMono] | |
| TI [TermTyped] | |
| TPTP [UntypedAST] | |
| TPTP_lexer | |
| TPTP_model_ast |
Simple Model AST
|
| TPTP_model_lexer | |
| TPTP_model_parser | |
| TPTP_parser | |
| TPTP_preprocess |
TPTP Preprocessor
|
| TPTP_print | |
| Task [Scheduling] | |
| Tbl [TermInner.UTIL] |
Hashtbl with terms as key.
|
| Tbl [TermInner.Util] | |
| Tbl [ID] | |
| TermInner |
Main View for terms
|
| TermMono |
top-level symbol
|
| TermTyped |
Terms with Types
|
| Time [Utils] | |
| Tip_ast |
Trivial AST for parsing
|
| Tip_lexer | |
| Tip_parser | |
| ToFO [TermMono] | |
| To_tptp [FO] |
Assume there are no types (other than `Unitype), no datatypes, no
pattern match...
|
| TransFO [TermMono] | |
| Transform |
Pipeline of Transformations
|
| Traversal |
Recursive Traversal of AST
|
| Ty [FO] | |
| TyBuiltin [TermMono] | |
| TyBuiltin [TermInner] | |
| TyBuiltin [FO] | |
| TypeCheck |
Type Checking of a problem
|
| TypeInference |
Scoping and Type Inference
|
| TypeMono |
Monomorphic Types
|
| TypePoly |
Types with polymorphism and meta-variables
|
| TypeUnify |
Unification of Types
|
U | |
| U [TermMono.OfFO] | |
| U [TermMono.ToFO] | |
| U [TermInner.Default] | |
| Unroll |
Unrolling of (Co)inductive Predicates
|
| UntypedAST |
Input AST
|
| Util [TermTyped] | |
| Util [TermInner] | |
| Util [Env] | |
| Util [FO] |
Utils
|
| UtilRepr [TermInner] |
Utils that only require a
TermInner.REPR
|
| Utils |
Utils
|
V | |
| Var [TypeMono] | |
| Var [TermMono] | |
| Var |
Variable
|
| VarSet [TermInner.UTIL_REPR] | |
| VarSet [TermInner.UtilRepr] | |
Z | |
| Z [Cardinality] |