A  
Arena 
Represent the game arena and operate on it.

ArenaParser  
Assignments 
Handling partial assignments of elements to variables.

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

B  
B [Matrix]  
BasicOperators [Aux]  
BigIntDiags [Diagram] 
Diagrams based on BigIntOrd.

BigIntOrd [Diagram] 
Variables module for integers using the bigger integer always.

Bitvector 
Bit vectors.

BoolFunction 
Represent Boolean functions.

BuiltinLang 
Basic builtin TRS language syntax.

C  
Class 
Represent regular classes of structures.

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

ContinuousRule 
Structure rewriting with continuous dynamics.

ContinuousRuleParser  
D  
DiagCons [Diagram.S] 
The consing module.

Diagram 
Ordered diagrams representing propositional formulas.

DiscreteRule 
Discrete structure rewriting rules construction and rewriting.

DiscreteRuleParser  
Distinguish 
Distinguish sets of structures by formulas.

E  
Elems [Structure] 
Sets of integers

F  
F [Matrix]  
FFTNF 
Computing the FF Type Normal Form.

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

FormulaCons [Formula] 
Hashconsed formula module.

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

FormulaOps 
Operations on formulas.

FormulaParser  
FormulaSubst 
Substitutions in formulas and realvalued expressions.

G  
GDL 
Game Description Language.

GDLParser  
GameSimpl 
Simplification of Toss games.

GameTree 
Game Tree used for choosing moves.

H  
H1 [HashCons.S] 
Hashtables with consed data as key (very efficient hashing).

H2 [HashCons.S] 
Hashtables with pairs of consed data as key (very efficient hashing).

HV [HashCons.S] 
Hashtables with pairs of consed data and other value as key.

HashCons 
Hashconsing module.

HashableTerm [Term]  
Heuristic 
Generate a heuristic from a payoff.

I  
I [Matrix]  
IntMap [Structure] 
Maps from int to 'alpha

IntMap [Aux]  
Integers 
Operations on arbitraryprecision integers, subset of Big_int module.

Ints [Aux]  
L  
LearnGame 
Module for learning games from examples.

LeftistPrioQueue [Aux]  
Lfp 
Learning LFP formulas.

M  
M [Solver] 
Interface to the solver.

Make [Diagram] 
Implementation of diagrams.

Make [HashCons] 
Functor to create the S module.

Matrix 
Compact matrix representation when Bigarray is available.

MiscNum 
Numeric support functions from Arith_flags and Int_misc OCaml modules.

N  
Numbers 
A smaller Num module, pure OCaml only.

O  
OrderedPoly 
Polynomials with ordered variables and integer coefficients.

OrderedPolySet 
Represent set of ordered polynomials and operate on it.

P  
P [Matrix]  
PSet [OrderedPolySet]  
ParseArc 
Contains the bottomup chartbased parser that uses syntax definitions
and checks if terms are welltyped when closing arcs.

Picture 
Processing pictures

Play 
Different play strategies.

Poly 
Represent polynomials as written and convert to ordered form.

Q  
QBF 
Quantified Boolean Formulas

QBFCons [QBF]  
R  
Rationals 
Operations on rational numbers, subset of the Ratio OCaml module.

RealExprCons [Formula] 
Hashconsed formula module.

RealQuantElim 
Simplify existentially quantified conjunction of polynomial inequalities.

RealQuantElimParser  
Reduction 
Reductions between structure classes and SO queries.

Rewriting 
Contains the functions responsible for rewriting and normalization.

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

SatSolver 
Interface to SAT solvers.

SignTable 
Handling sign tables for quantifier elimination.

SimplePrioQueue [Aux]  
Solver 
Solver for checking if formulas hold on structures.

StrMap [Aux]  
StringMap [Structure] 
Maps from string to 'alpha

Strings [Aux]  
Structure 
Representing relational structures with realvalued functions.

StructureParser  
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.

T  
TRS 
Get syntax definitions from a TRS.

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

TermHashtbl [Term]  
Terms [GDL]  
TranslateFormula 
Translating formulas from GDL to Toss.

TranslateGame 
Translating games from GDL to Toss.

Tuples [GDL]  
Tuples [Structure] 
Sets of tuples of ints

W  
WeightDiags [Diagram] 
Diagrams based on WeightIntOrd.

WeightIntOrd [Diagram] 
Variables module for integers using the weights.
