This library contains the core data structures and algorithms for manipulating Nunchaku's terms, statements and models, as well as many utilities.
| AnalyzeType |
Analyze Types : Cardinalities, Abstract, Incomplete
|
| Cardinality |
Cardinalities
|
| Env |
Environment
|
| FO |
First-Order Monomorphic Terms and Formulas
|
| FO_rel |
Relational FO Logic
|
| FO_tptp |
TPTP representation
|
| ID |
Unique Identifiers
|
| Intf |
Interfaces
|
| Lazy_list |
Lazy List
|
| Location |
Location in a file
|
| MetaVar |
Variables for Mutable Unification
|
| Model |
Model
|
| Pattern |
Pattern
|
| Polarity |
Polarity
|
| Prelude |
Prelude
|
| Problem |
Top-Level Statements (with locations)
|
| ProblemMetadata |
Metadata attached to Problem
|
| Reduce |
Reductions, including Beta Reduction
|
| Scheduling |
Scheduling of sub-processes
|
| Sexp_lib |
Simple and efficient S-expression parsing/printing
|
| Signature |
Signature
|
| Statement |
Top-level statement
|
| TermInner |
Main View for terms
|
| TermMono |
top-level symbol
|
| TermTyped |
Terms with Types
|
| Transform |
Pipeline of Transformations
|
| Traversal |
Recursive Traversal of AST
|
| TypeCheck |
Type Checking of a problem
|
| TypeMono |
Monomorphic Types
|
| TypePoly |
Types with polymorphism and meta-variables
|
| TypeUnify |
Unification of Types
|
| UntypedAST |
Input AST
|
| Utils |
Utils
|
| Var |
Variable
|
This library contains transformations from problems to problems, most of which are encodings.
| 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"
|
| FoToRelational |
FOL to Relational FO Logic
|
| IntroGuards |
Introduce Guards
|
| LambdaLift |
Lambda Lifting
|
| Model_clean |
Cleanup models
|
| Monomorphization |
Monomorphization
|
| Polarize |
Polarize
|
| Skolem |
Skolemization
|
| Specialize |
Specialization
|
| TypeInference |
Scoping and Type Inference
|
| Unroll |
Unrolling of (Co)inductive Predicates
|
Parsers and printers for several formats, including Nunchaku's native format.
| Ast_kodkod |
Trivial AST for Kodkod models
|
| Lex_kodkod | |
| Lexer |
Lexer
|
| Parse_kodkod | |
| Parse_tip |
Wrapper for TIP
|
| Parser | |
| Parsing_utils |
Various Utils for Parsing
|
| TPTP_lexer | |
| TPTP_model_ast |
Simple Model AST
|
| TPTP_model_lexer | |
| TPTP_model_parser | |
| TPTP_parser | |
| TPTP_preprocess |
TPTP Preprocessor
|
| TPTP_print | |
| Tip_ast |
Trivial AST for parsing
|
| Tip_lexer | |
| Tip_parser |