Auxiliary functions that operate on standard library data structures and standard library-like definitions.

Hash-consing module.

Represent formulas with first-order, mso, and real variables.

Maps, iterators and folds over formulas and real-valued expressions.

Substitutions in formulas and real-valued expressions.

Interface to SAT solvers.

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

Quantified Boolean Formulas

Represent Boolean functions.

Ordered diagrams representing propositional formulas.

Computing the FF Type Normal Form.

Operations on formulas.

Numeric support functions from Arith_flags and Int_misc OCaml modules.

Operations on arbitrary-precision integers, subset of Big_int module.

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

A smaller Num module, pure OCaml only.

Representing relational structures with real-valued functions.

Handling partial assignments of elements to variables.

Polynomials with ordered variables and integer coefficients.

Represent set of ordered polynomials and operate on it.

Represent polynomials as written and convert to ordered form.

Handling sign tables for quantifier elimination.

Simplify existentially quantified conjunction of polynomial inequalities.

Solver for checking if formulas hold on structures.

Represent regular classes of structures.

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

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.

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

Basic built-in TRS language syntax.

Contains the functions responsible for rewriting and normalization.

Contains the bottom-up chart-based parser that uses syntax definitions and checks if terms are well-typed when closing arcs.

Get syntax definitions from a TRS.

Discrete structure rewriting rules construction and rewriting.

Structure rewriting with continuous dynamics.

Represent the game arena and operate on it.

Generate a heuristic from a payoff.

Game Tree used for choosing moves.

Different play strategies.

Game Description Language.

Translating formulas from GDL to Toss.

Translating games from GDL to Toss.

Simplification of Toss games.

Learning LFP formulas.

Reductions between structure classes and SO queries.

Distinguish sets of structures by formulas.

Module for learning games from examples.

Compact matrix representation when Bigarray is available.

Aux	Auxiliary functions that operate on standard library data structures and standard library-like definitions.
HashCons	Hash-consing module.
Formula	Represent formulas with first-order, mso, and real variables.
FormulaParser
FormulaMap	Maps, iterators and folds over formulas and real-valued expressions.
FormulaSubst	Substitutions in formulas and real-valued 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 arbitrary-precision 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 real-valued 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 built-in TRS language syntax.
Rewriting	Contains the functions responsible for rewriting and normalization.
ParseArc	Contains the bottom-up chart-based parser that uses syntax definitions and checks if terms are well-typed 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