Aux 
Auxiliary functions that operate on standard library data
structures and standard librarylike definitions.

HashCons 
Hashconsing module.

Formula 
Represent formulas with firstorder, mso, and real variables.

FormulaParser  
FormulaMap 
Maps, iterators and folds over formulas and realvalued expressions.

FormulaSubst 
Substitutions in formulas and realvalued expressions.

SatSolver 
Interface to SAT solvers.

Sat 
Basic interface to a sat solver and convertion between cnf and dnf formulas.

QBF 
Quantified Boolean Formulas

BoolFunction 
Represent Boolean functions.

Diagram 
Ordered diagrams representing propositional formulas.

FFTNF 
Computing the FF Type Normal Form.

FormulaOps 
Operations on formulas.

MiscNum 
Numeric support functions from Arith_flags and Int_misc OCaml modules.

Bitvector 
Bit vectors.

Integers 
Operations on arbitraryprecision integers, subset of Big_int module.

Rationals 
Operations on rational numbers, subset of the Ratio OCaml module.

Numbers 
A smaller Num module, pure OCaml only.

Structure 
Representing relational structures with realvalued functions.

StructureParser  
Assignments 
Handling partial assignments of elements to variables.

OrderedPoly 
Polynomials with ordered variables and integer coefficients.

OrderedPolySet 
Represent set of ordered polynomials and operate on it.

Poly 
Represent polynomials as written and convert to ordered form.

SignTable 
Handling sign tables for quantifier elimination.

RealQuantElim 
Simplify existentially quantified conjunction of polynomial inequalities.

RealQuantElimParser  
Solver 
Solver for checking if formulas hold on structures.

Class 
Represent regular classes of structures.

ClassParser  
Term 
The type of term types, operations on these types and a parser for types.

SyntaxDef 
Contains the type of syntax elements and definitions, basic functions
for syntax definitions and printing with names generated from syntax
definitions and a few basic syntax definitions of types and constructors.

Coding 
Contains the type of typed terms, functions calculating type and
reconstruction for a term, and printing and parsing for terms.

BuiltinLang 
Basic builtin TRS language syntax.

Rewriting 
Contains the functions responsible for rewriting and normalization.

ParseArc 
Contains the bottomup chartbased parser that uses syntax definitions
and checks if terms are welltyped when closing arcs.

TRS 
Get syntax definitions from a TRS.

DiscreteRule 
Discrete structure rewriting rules construction and rewriting.

DiscreteRuleParser  
ContinuousRule 
Structure rewriting with continuous dynamics.

ContinuousRuleParser  
Arena 
Represent the game arena and operate on it.

ArenaParser  
Heuristic 
Generate a heuristic from a payoff.

GameTree 
Game Tree used for choosing moves.

Play 
Different play strategies.

GDL 
Game Description Language.

GDLParser  
TranslateFormula 
Translating formulas from GDL to Toss.

TranslateGame 
Translating games from GDL to Toss.

GameSimpl 
Simplification of Toss games.

Lfp 
Learning LFP formulas.

Reduction 
Reductions between structure classes and SO queries.

Distinguish 
Distinguish sets of structures by formulas.

LearnGame 
Module for learning games from examples.

Matrix 
Compact matrix representation when Bigarray is available.

Picture 
Processing pictures
