Index of types

abstract_game_tree [GameTree]
Abstract game tree, just stores state and move information.
add_to_decls [Term]
Adding a declaration to a well-formed set of declarations.
argpaths [GDL]
The integers should be all-distinct and from 0 to N-1.
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]

big_int [Integers]
The type of big integers.
bitvector [Bitvector]
bool_def [BoolFunction]
Boolean definition of a function, knows whether it is a fixed-point.
bool_formula [QBF]
bool_function [BoolFunction]
This type describes Boolean functions

choice [Aux]
clause [GDL]
const_or_fo_var [Formula]
const_var [Formula]

data [HashCons.S]
decls_set [Term]
Data associated with a well-formed 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.

elt [Matrix.MAT]
eq_sys [Formula]
Equation system: a left-hand-side f,a actually represents Fun (f, `FO a)

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.

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 expanded-out.
gdl_translation [TranslateGame]
Data to be used when translating moves.
graph [GDL]

hc [HashCons]
The type of hash-consed values, inspired by Filliatre's work.
hc_formula [Formula]
hc_real_expr [Formula]

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]

key [Term.TermHashtbl]

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]

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.

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

other_value [HashCons.S]

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]

qbf [QBF]
qbf_raw [QBF]
Type for Quantified Boolean Formulas.

ratio [Rationals]
raw_formula [Formula]
The raw and hash-consed types.
raw_real_expr [Formula]
real_expr [Formula]
Real-valued 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 formula-based rewrite rule representation.

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 [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_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]

value [SatSolver]
F | T | X
var [Diagram.S]
var [SatSolver.S]
var [Formula]
What we call variables can be a constant, a first-order variable, a second-order variable, or a real-valued variable.
var_tuples [DiscreteRule]