Auxiliary functions that operate on standard library data structures and standard library-like definitions.
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.