A  
abstract_game_tree [GameTree] 
Abstract game tree, just stores state and move information.

add_to_decls [Term] 
Adding a declaration to a wellformed set of declarations.

argpaths [GDL] 
The integers should be alldistinct and from 0 to N1.

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

assignment_set [Assignments] 
We represent assignment sets as trees.

atom [GDL]  
B  
big_int [Integers] 
The type of big integers.

bitvector [Bitvector]  
bool_def [BoolFunction] 
Boolean definition of a function, knows whether it is a fixedpoint.

bool_formula [QBF]  
bool_function [BoolFunction] 
This type describes Boolean functions

C  
choice [Aux]  
clause [GDL]  
const_or_fo_var [Formula]  
const_var [Formula]  
D  
data [HashCons.S]  
decls_set [Term] 
Data associated with a wellformed set of declarations; expected
to grow monotonically by adding new declarations.

def_branch [GDL]  
definition [Arena] 
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.

diag [Diagram]  
diag_raw [Diagram] 
Diagrams represent propositional formulas as printed by diag_str.

E  
elt [Matrix.MAT]  
eq_sys [Formula] 
Equation system: a lefthandside
f,a actually represents
Fun (f, `FO a)

F  
fo_var [Formula]  
formula [Formula] 
This type describes formulas of relational logic with equality.

formula_and_expr_fold [FormulaMap] 
Generalized fold over formula and real expression types.

formula_and_expr_map [FormulaMap] 
Generalized map over formula and real expression types.

fun_definition [Coding] 
The type of Function Definitions.

G  
game [Arena] 
The basic type of Arena.

game_state [Arena] 
State of the game.

game_tree [GameTree]  
gdl_defs [GDL]  
gdl_rule [GDL] 
Positive and negative literals separated, disjunctions expandedout.

gdl_translation [TranslateGame] 
Data to be used when translating moves.

graph [GDL]  
H  
hc [HashCons] 
The type of hashconsed values, inspired by Filliatre's work.

hc_formula [Formula]  
hc_real_expr [Formula]  
I  
isubsts [Term]  
iter_s_subst [Term] 
Iterated substitutions are sets of term equations in solved
form, but without disjointness between the domain and variables
in the image of substitution.

iter_t_subst [Term]  
K  
key [Term.TermHashtbl]  
L  
label [Arena] 
A single move consists of applying a rewrite rule for a time from the
time_in interval, and parameters from the interval list.

lit [SatSolver.S]  
literal [GDL]  
logic [Distinguish]  
M  
matching [DiscreteRule] 
Single match of a rule, and a set of matches.

matchings [DiscreteRule]  
matrix_bool [Matrix]  
matrix_float [Matrix]  
matrix_int [Matrix]  
move [Arena] 
Move  complete basic action data.

N  
node_info [GameTree] 
The general information in a game tree node.

num [Numbers]  
O  
other_value [HashCons.S]  
P  
parser_arc [ParseArc] 
Incomplete arcs that appear during parsing.

parser_elem [ParseArc] 
The type of elements created during parsing.

path [GDL]  
path_set [GDL]  
picture [Picture]  
player_loc [Arena] 
A game has locations.

polynomial [Poly]  
polynomial [OrderedPoly]  
position [Term] 
Positions, in supertypes.

prolog_program [GDL]  
pset [OrderedPolySet]  
Q  
qbf [QBF]  
qbf_raw [QBF] 
Type for Quantified Boolean Formulas.

R  
ratio [Rationals]  
raw_formula [Formula] 
The raw and hashconsed types.

raw_real_expr [Formula]  
real_expr [Formula] 
Realvalued terms allow counting, characteristic functions, arithmetic.

real_var [Formula]  
reduction [Reduction] 
Reduction with definitions for relations and constants.

rel_atom [GDL]  
request [GDL]  
rewrite_rule [Coding] 
The type of Rewriting Rules.

rrules_set [Rewriting] 
A set of rewriting rules.

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

rule [DiscreteRule] 
The formulabased rewrite rule representation.

S  
s_subst [Term]  
sdef_result [SyntaxDef] 
Supertypes and whether we define a variable.

set_list [Assignments] 
Helper type to represent a set or a list of elements with length.

sign_op [Formula] 
Sign operands.

so_var [Formula]  
solution [SatSolver]  
split_result [Aux] 
Type for some split results.

struc_rule [DiscreteRule] 
Specification of a discrete rewriting rule, as in modelling
document.

struct_sum [Class] 
Sum of structures or specified classes with relation replacements.

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

structure_class [Class] 
Class of regular structures.

substitution [GDL]  
substs [Term]  
syntax_def [SyntaxDef] 
Grammar rules for functor terms (functions/constants/classes), for
(sharing) variables and for type variables.

syntax_elem [SyntaxDef] 
Elements of the "right hand side" of a grammar rule.

T  
t [Matrix.MAT]  
t [Term.TermHashtbl]  
t [Term.HashableTerm]  
t [OrderedPoly] 
to be compatible with OrderedType signature

t [Diagram.Variables]  
t [Diagram.S]  
t [HashCons.Type]  
t [HashCons.S]  
t [Aux.PRIOQUEUE]  
t_raw [Diagram.S]  
t_subst [Term] 
Substitutions are kept abstract to make it easier to evolve term
semantics.

term [GDL]  
term [Term] 
Hierarchical terms.

terminal_info [GameTree]  
topol_sort_ops [Aux] 
Operations for imperatively manipulating the graph for
Aux.topol_sort .

tossrule_data [TranslateGame]  
transl_data [TranslateFormula]  
trs [TRS]  
V  
value [SatSolver] 
F  T  X

var [Diagram.S]  
var [SatSolver.S]  
var [Formula] 
What we call variables can be a constant, a firstorder variable,
a secondorder variable, or a realvalued variable.

var_tuples [DiscreteRule] 