Index of types

Abstract game tree, just stores state and move information.

Adding a declaration to a well-formed set of declarations.

The integers should be all-distinct and from 0 to N-1.

two heuristics for selecting defined relations: select relations with arity smaller than three; or, select relations that have ground defining clauses (i.e.

We represent assignment sets as trees.

The type of big integers.

Boolean definition of a function, knows whether it is a fixed-point.

This type describes Boolean functions

Data associated with a well-formed set of declarations; expected to grow monotonically by adding new declarations.

The order of following entries matters: DefPlayers adds more players, with consecutive numbers starting from first available; later StartStruc, CurrentStruc, StateTime and StateLoc entries override earlier ones; later DefLoc with already existing location ID replaces the earlier one.

Diagrams represent propositional formulas as printed by diag_str.

Equation system: a left-hand-side f,a actually represents Fun (f, `FO a)

This type describes formulas of relational logic with equality.

Generalized fold over formula and real expression types.

Generalized map over formula and real expression types.

The type of Function Definitions.

The basic type of Arena.

State of the game.

Positive and negative literals separated, disjunctions expanded-out.

Data to be used when translating moves.

The type of hash-consed values, inspired by Filliatre's work.

Iterated substitutions are sets of term equations in solved form, but without disjointness between the domain and variables in the image of substitution.

A single move consists of applying a rewrite rule for a time from the time_in interval, and parameters from the interval list.

Single match of a rule, and a set of matches.

Move - complete basic action data.

The general information in a game tree node.

Incomplete arcs that appear during parsing.

The type of elements created during parsing.

A game has locations.

Positions, in supertypes.

Type for Quantified Boolean Formulas.

The raw and hash-consed types.

Real-valued terms allow counting, characteristic functions, arithmetic.

Reduction with definitions for relations and constants.

The type of Rewriting Rules.

A set of rewriting rules.

Specification of a continuous rewriting rule, as in modelling document.

The formula-based rewrite rule representation.

Supertypes and whether we define a variable.

Helper type to represent a set or a list of elements with length.

Sign operands.

Type for some split results.

Specification of a discrete rewriting rule, as in modelling document.

Sum of structures or specified classes with relation replacements.

Elements are internally represented by integers, bu the structure also stores a naming of elements.

Class of regular structures.

Grammar rules for functor terms (functions/constants/classes), for (sharing) variables and for type variables.

Elements of the "right hand side" of a grammar rule.

to be compatible with OrderedType signature

Substitutions are kept abstract to make it easier to evolve term semantics.

Hierarchical terms.

Operations for imperatively manipulating the graph for Aux.topol_sort.

F | T | X

What we call variables can be a constant, a first-order variable, a second-order variable, or a real-valued variable.