Index of modules

Represent the game arena and operate on it.

Handling partial assignments of elements to variables.

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

Diagrams based on BigIntOrd.

Variables module for integers using the bigger integer always.

Bit vectors.

Represent Boolean functions.

Basic built-in TRS language syntax.

Represent regular classes of structures.

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

Structure rewriting with continuous dynamics.

The consing module.

Ordered diagrams representing propositional formulas.

Discrete structure rewriting rules construction and rewriting.

Distinguish sets of structures by formulas.

Sets of integers

Computing the FF Type Normal Form.

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

Hash-consed formula module.

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

Operations on formulas.

Substitutions in formulas and real-valued expressions.

Game Description Language.

Simplification of Toss games.

Game Tree used for choosing moves.

Hashtables with consed data as key (very efficient hashing).

Hashtables with pairs of consed data as key (very efficient hashing).

Hashtables with pairs of consed data and other value as key.

Hash-consing module.

Generate a heuristic from a payoff.

Maps from int to 'alpha

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

Module for learning games from examples.

Learning LFP formulas.

Interface to the solver.

Implementation of diagrams.

Functor to create the S module.

Compact matrix representation when Bigarray is available.

Numeric support functions from Arith_flags and Int_misc OCaml modules.

A smaller Num module, pure OCaml only.

Polynomials with ordered variables and integer coefficients.

Represent set of ordered polynomials and operate on it.

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

Processing pictures

Different play strategies.

Represent polynomials as written and convert to ordered form.

Quantified Boolean Formulas

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

Hash-consed formula module.

Simplify existentially quantified conjunction of polynomial inequalities.

Reductions between structure classes and SO queries.

Contains the functions responsible for rewriting and normalization.

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

Interface to SAT solvers.

Handling sign tables for quantifier elimination.

Solver for checking if formulas hold on structures.

Maps from string to 'alpha

Representing relational structures with real-valued functions.

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.

Get syntax definitions from a TRS.

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

Translating formulas from GDL to Toss.

Translating games from GDL to Toss.

Sets of tuples of ints

Diagrams based on WeightIntOrd.

Variables module for integers using the weights.