( * ) [Matrix.MAT]  
( */ ) [Numbers]  
(&&&) [Bitvector] 
Bitwise and.

(+) [Matrix.MAT]  
(+/) [Numbers]  
() [Matrix.MAT]  
(/) [Numbers]  
() [Aux.BasicOperators] 
Function composition.

(/) [Matrix.MAT]  
(//) [Numbers]  
(</) [Numbers]  
(<=/) [Numbers]  
(<>/) [Numbers]  
(<) [Aux.BasicOperators]  
(=/) [Numbers]  
(>/) [Numbers]  
(>=/) [Numbers]  
() [Bitvector] 
Bitwise or.

(~) [Matrix.MAT]  
A  
abs_big_int [Integers] 
Absolute value.

abs_num [Numbers] 
Absolute value.

abs_ratio [Rationals]  
abstract_learn [Lfp] 
Abstract learning: teacher takes a tuple of relation names and formulas and
gives a counterexample structure with these relations where the given
formulas are supposed to hold (but differ from the given).

add [Term.TermHashtbl]  
add [OrderedPolySet]  
add [OrderedPoly]  
add_big_int [Integers] 
Addition.

add_big_int_ratio [Rationals]  
add_clause [SatSolver.S]  
add_constant [Structure] 
Add a new constant.

add_def_funs [Solver] 
Add defined functions to a structure.

add_def_rels [Solver] 
Add defined relations to a structure.

add_elem [Structure] 
Add element
e to struc if it is not yet there.

add_elems [Structure]  
add_first_rule [Rewriting] 
Add a rewriting rule: whether the rewritten term has to be ground,
LHS and RHS  to the set, at the start.

add_fun [Structure] 
Add function assignment
e > x to function fn in structure struc .

add_funs [Structure] 
Add function assignments
assgns to fn in structure struc .

add_int_big_int [Integers] 
Addition of a small integer to a big integer.

add_int_ratio [Rationals]  
add_ints [Aux]  
add_last_rule [Rewriting] 
Add a rewriting rule to the set, at the end.

add_logic_name [Term] 
Logic names are functors whose terms should not decompose under
unification or ISA relation and its algorithms.

add_models [Structure] 
Assign models to elements by
f in struc , replacing previous.

add_new_elem [Structure] 
Add new element to
struc , return the updated structure and the
element.

add_path [GDL]  
add_quantifier [SatSolver.S]  
add_ratio [Rationals]  
add_rel [Structure] 
Add tuple
tp to relation rn in structure struc .

add_rel_name [Structure] 
Ensure relation named
rn exists in struc , add if needed.

add_rel_named_elems [Structure] 
Add tuple
tp to relation rn in structure struc .

add_rels [Structure] 
Add tuples
tps to relation rn in structure struc .

add_strings [Aux]  
add_terms [GDL]  
add_to_decls [Term] 
Assuming that the given set of declarations is wellformed, check
if it will remain wellformed after adding the given declaration.

add_to_maximal [Aux] 
Assuming that
l2 already has only maximal elements,
add_to_maximal cmp l1 l2 computes maximal cmp (l1 @ l2) .

add_tuples [Structure]  
additional_xslt_name [BuiltinLang]  
additional_xslt_rules [Coding]  
all_fluents [Arena]  
all_ntuples [Aux] 
An
n th cartesian power of the list.

all_subsets [Aux] 
All subsets of a given
set of size up to max_size .

all_vars [FormulaSubst] 
All variables in a formula.

apply_defs [BoolFunction] 
Insert nonfixedpoint definitions into a function.

apply_isbs [Term]  
apply_rewrite [Arena]  
apply_rule_int [Arena]  
apply_s [Coding]  
apply_sbs [Term]  
apply_to_side [ContinuousRule] 
Apply
f to left (if to_left ) or right side of the given rule.

approx_big_int [Integers]  
approx_printing_flag [MiscNum]  
approx_ratio_exp [Rationals]  
approx_ratio_fix [Rationals]  
approximate_monotonic [DiscreteRule] 
If
true , ignore what happens on RHSes of rules when assessing
if fluents are positive / negative (only check whether their
LHS+precondition occurrences are negative/positive).

array_argfind [Aux]  
array_argfind_all [Aux]  
array_argfind_all_max [Aux]  
array_argfindi [Aux]  
array_combine [Aux] 
Zip two arrays into an array of pairs.

array_exists [Aux]  
array_existsi [Aux]  
array_find_all [Aux] 
Find all elements for which
f holds.

array_find_all_max [Aux] 
Find indices of all maximal elements in an array.

array_fold_left2 [Aux] 
Foldleft on two arrays.

array_fold_map2 [Aux] 
Foldleft and map on two arrays.

array_foldi_left [Aux] 
As
Array.fold_left , but with the element position passed.

array_for_all [Aux] 
Find if a predicate holds for all elements.

array_for_all2 [Aux] 
For all on two arrays.

array_for_alli [Aux] 
Find if a positiondependent predicate holds for all elements.

array_fprint [Aux]  
array_from_assoc [Aux] 
Make an array from an association from indices to values.

array_iter2 [Aux] 
Iterate an action over all elements of two arrays
pointwise.

array_map2 [Aux] 
Map a function over two arrays indexwise.

array_map_of_list [Aux] 
Same as
Array.of_list (List.map f l)

array_map_some [Aux] 
Map an array filtering out some elements.

array_mapi_some [Aux]  
array_mem [Aux]  
array_of_players [Arena]  
array_replace [Aux] 
Return a copy of
array with the i th element replaced by elem .

as_conjuncts [FormulaOps] 
Formula as a list of conjuncts, with one level of distributing
negation over disjunction and pushing quantifiers inside.

as_defined_rels [TranslateGame]  
assign_emptyset [FormulaSubst] 
Assign emptyset to an MSOvariable.

assign_name [BuiltinLang]  
assign_name [Term]  
assigned_elems [Assignments] 
Elements assigned to a given FO variable.

assigned_vars [Assignments] 
Variables assigned in an assignement set.

assignments_of_list [Assignments] 
Create an assignment set out of an array of variables and a list of
assigned tuples.

assoc_all [Aux] 
Return all values of a key.

assoc_s_sb [Term]  
assoc_t_sb [Term]  
at_path [GDL] 
Find the subterm at given path, if the term does not have the
path, raise
Not_found ; at_path p t is $t \tpos p$.

at_paths [GDL] 
Find the list of subterms at paths from the given set, if the term
does not have some of the paths, ignore them if
~fail_at_missing:false ,
raise Not_found if ~fail_at_missing:true .

atom_of_rel [GDL] 
Remember that
rel_of_atom inverts polarity of "distinct" 
invert back after using atom_of_rel if needed.

atom_str [GDL]  
atoms [Distinguish] 
The list of literals which hold for a tuple on a structure,
i.e.

atoms [FormulaOps] 
All atoms over given signature and variables.

atoms_of_body [GDL]  
atp [FormulaOps] 
AType with variables over given relations, no repetition, equality.

aux_glb [Term]  
aux_glb_lub_cont [Term]  
aux_isa_unify [Term]  
aux_lub [Term]  
aux_mgu_i [Term]  
aux_mgu_i_cont [Term]  
B  
base_power_big_int [Integers]  
basic_outline [Lfp] 
Basic outline of the form "ex x_1 ..

basic_system [TRS]  
bf_str [QBF] 
Print a Boolean formula as a string.

bigSIZE [Diagram] 
Suitable big size for hash modules.

big_int_of_int [Integers] 
Convert a small integer to a big integer.

big_int_of_nat [Integers] 
Convert a natural to a big integer.

big_int_of_ratio [Rationals]  
big_int_of_string [Integers] 
Convert a string to a big integer, in decimal.

biggest_int [MiscNum]  
binary_abs [QBF] 
Given a signed binary number n returns n.

binary_add [QBF] 
Binary addition.

binary_minus [QBF] 
Given (binary) number n returns n in our (2complement) representation.

binary_sub [QBF] 
Binary subtraction.

bit_0_cons_name [BuiltinLang]  
bit_1_cons_name [BuiltinLang]  
bit_name [BuiltinLang]  
bit_sd [BuiltinLang]  
bit_tp [BuiltinLang]  
bits_to_int [Coding]  
black_n_white [Picture] 
Colorencode numbers, 0 remains black, possible clashes.

blank [GDL]  
blank_out [TranslateFormula]  
blank_outside_subterm [GDL]  
blank_outside_subterms [GDL]  
board_coords_name [Structure] 
Board element name under given coordinates, column first.

board_elem_coords [Structure] 
Coordinates, column first, of a board element name.

boolean_false_name [BuiltinLang]  
boolean_false_sd [BuiltinLang]  
boolean_name [BuiltinLang]  
boolean_sd [BuiltinLang]  
boolean_tp [BuiltinLang]  
boolean_true_name [BuiltinLang]  
boolean_true_sd [BuiltinLang]  
brackets_name [BuiltinLang]  
brackets_rules [Coding]  
brightness [Picture] 
Floatingpoint matrix of brightness in range
0..1 .

build [Diagram.S] 
Import from unordered generic type.

build_cases [SignTable] 
Build array of polynomials and cases to check given set of polynomials.

build_defrels [TranslateFormula]  
build_graph [GDL]  
build_rule_s [DiscreteRule]  
builtin_decls [ParseArc]  
C  
cAnd [Diagram.S]  
cAnd [Formula] 
Hashcons a conjunction.

cEmpty [Diagram.S] 
Smart constructors, cAnd hashes and enforces the assertions (0)  (4).

cGRID_SIZE [Arena] 
Default number of sample points per parameter in tree search.

cPAYOFF_AS_HEUR [GameTree] 
How to exchange payoffs for heuristics.

cUnit [Diagram.S]  
cache_expanded_form [Heuristic] 
This function allows to add cached expanded forms; for speed only!

cancel_timeout [Play]  
canny [Picture] 
Detect edges:
hi_thr how insensitive to new edges,
lo_thr how insensitive to edge continuations,
extend how many pixels to prolong existing edge.

cardinal [OrderedPolySet]  
case_str [RealQuantElim]  
case_str [SignTable]  
cases_str [RealQuantElim]  
ceiling_ratio [Rationals]  
change_fun [Structure] 
Change function
fn assignment for element e to x in struc .

change_fun_int [Structure]  
changeable_rels [DiscreteRule] 
Relations that can explicitly change state by rewriting (i.e.

char_cons_name [BuiltinLang]  
char_name [BuiltinLang]  
char_tp [BuiltinLang]  
check [Class]  
check [Solver.M] 
Check the formula on the structure.

check_reduct [Reduction] 
Check if
reduct is a correct reduction of dimention dim from class
defined by cfrom to one given by cto , on structures of size size .

check_rel [Structure] 
Check if a relation holds for a tuple.

check_sign [SignTable] 
Check if given float has sign as required by the sign_op.

check_tp [Coding] 
Check whether the term belongs to the given class.

choose_fo [Assignments] 
Select an arbitrary assignment for firstorder variables with the
given names and default values.

choose_match [DiscreteRule] 
Choose an arbitrary embedding of a rule from the matchings
returned by
DiscreteRule.find_matchings for the same structure and rewrite
rule.

choose_moves [GameTree] 
Choose all maximizing moves given a game tree.

clause_str [GDL]  
clause_str [Sat] 
Return the given clause (disjunction of literals) as string.

clause_vars [GDL]  
clauses_str [GDL]  
clauses_vars [GDL]  
clean_name [Aux] 
Changes a string
s to use only alphanumeric characters and underscore
and to start with a lowercase letter.

clear [Term.TermHashtbl]  
clear [Diagram.S] 
Clears the hash table.

clear [HashCons.S] 
Clear the given hashconsing table.

clear_bit [Bitvector] 
Clear the bit at the given position, i.e.

clear_cache [Solver] 
Clear cache.

clear_fun [Structure] 
Remove the given function from
struc .

clear_names [Structure] 
Remove element names from structure.

clear_qbf_consing [QBF] 
Clear QBF consing table  only for strict test repeatability.

clear_rels [Structure] 
Remove all relations matching the predicate.

clear_timeout [Solver.M] 
Clear timeout function.

clear_timeout [Sat] 
Clear timeout function.

close_arc [ParseArc] 
Closes an arc when it is completed: returns the corresponding term
parser element together with the starting position of the arc.

close_context_name [BuiltinLang]  
closure [OrderedPolySet] 
Closure of a set of polynomials
polys under the operations: extracting the leading coefficient (if deg > 0), omitting the leading term (if deg > 0), taking the derivative (if deg > 0), taking the modified remainder MR(p, q) for deg p >= deg q.
Return resulting polynomials of degree 0 and greater separately.

cmp_weight [Diagram] 
Compare by weight if present in array, else simply the natural order.

cnf_str [Sat] 
Return the given CNF formula as string.

code_as_term_name [BuiltinLang]  
code_bit [Coding]  
code_bool [Coding]  
code_char [Coding]  
code_fun_definition [Coding]  
code_hlist [Coding]  
code_input_rewrite_rule [Coding]  
code_list [Coding]  
code_priority_input_rewrite_rule [Coding]  
code_rewrite_rule [Coding]  
code_string [Coding]  
code_syntax_definition [Coding]  
code_syntax_element_list [Coding]  
code_term [Coding]  
code_term_incr_vars [Coding]  
collect [Aux] 
Collects elements by key (returns a list sorted by key).

colorcode [Picture]  
colorful [Picture]  
compare [OrderedPoly]  
compare [Structure] 
Equality check on structures.

compare [Diagram.Variables]  
compare [Formula] 
Compare two formulas.

compare_big_int [Integers]  compare_big_int a b returns 0 if a and b are equal,
1 if a is greater than b , and 1 if a is smaller than b .

compare_big_int_ratio [Rationals]  
compare_diff [Arena] 
Compare two (game, state) pairs and explain the first difference
met.

compare_diff [ContinuousRule] 
Compare two rules and explain the first difference
met.

compare_diff [DiscreteRule] 
Compare two rules and explain the first difference
met.

compare_diff [Structure] 
Compare two structures and explain the first difference met.

compare_elems [Structure] 
Comparison function for elements.

compare_int [MiscNum]  
compare_num [Numbers]  
compare_ratio [Rationals]  
compare_re [Formula] 
Compare two real expressions.

compare_types [Distinguish] 
Order on types that we use to select the minimal ones.

compare_var_lists [Formula]  
compare_var_tups [Formula]  
compare_vars [Assignments] 
The order on variables we use; might differ from Formula.compare_vars!

compare_vars [Formula] 
Compare two variables.

compile [Formula] 
Compile eq_sys to function.

compile_formula_rule [DiscreteRule]  
compile_rule [DiscreteRule] 
Translate a rule specification into a processed form.

complement [Assignments] 
Complement an assignment set assuming
elems are all assignable elements.

complement_join [Assignments] 
Complement
a and join with aset ; assumes a is joined with aset

complete_paths_for [GDL] 
Check whether each of argpaths covers some tree in c_paths
completely.

compress [Assignments] 
Compress the given assignment set, use number of elements.

compute_heuristic [Heuristic] 
Helper function to do the full computation.

concat_foldl [Aux]  concat_foldl f (a::l) init = concat_foldl f l (concat_map (f a) init)

concat_foldr [Aux] 
Another very useful function from the list monad family:
concat_foldr f (a::l) init = concat_map (f a) (concat_foldr f l init)

concat_map [Aux] 
Concatenate results of a function.

conjunct_str [Sat] 
Return the given conjunction of literals as string.

cons [Aux]  cons e l = e::l .

const [OrderedPoly] 
Constructur 'Const' but taking normal integers.

const_coeff [OrderedPoly]  
const_or_fo_var_of_string [Formula]  
const_var_of_string [Formula]  
constant_factors [OrderedPoly]  
constant_value [OrderedPoly]  
constants [Structure] 
Return the assignment of constants in the structure.

convert [QBF] 
Convert a QBF to CNF.

convert [Sat] 
Convert a DNF formula to CNF (or equivalently, CNF to DNF).

convert_aux_cnf [Sat] 
Convert a auxiliary CNF formula to "real" CNF (or, equivalently, to DNF).

convolution [Picture] 
Discrete 2D convolution: around each point of
image , sum all elements
of the product of filter and corresponding image elements.

convolve [QBF] 
Convolve a NxNxL+1 list of (signed) weights with a list of L bitimages
of size XxY.

copy [Term.TermHashtbl]  
counter_n [GDL]  
create [Term.TermHashtbl]  
create [HashCons.S] 
Create a new hashconsing table of the given size.

create_arc [ParseArc]  
create_decls [Term]  
create_from_lists [Structure]  
create_from_lists_position [Structure]  
create_from_lists_range [Structure]  
create_normalized_ratio [Rationals]  
create_ratio [Rationals]  
D  
dag_str [QBF] 
Print a QBF formula as a dag.

decode_bit [Coding]  
decode_bit_list [Coding]  
decode_bool [Coding]  
decode_char [Coding]  
decode_fun_definition [Coding]  
decode_hlist [Coding]  
decode_hlist_opt [Coding]  
decode_input_rewrite_rule [Coding]  
decode_list [Coding]  
decode_list_opt [Coding]  
decode_priority_input_rewrite_rule [Coding]  
decode_rewrite_rule [Coding]  
decode_string [Coding]  
decode_string_opt [Coding]  
decode_syntax_definition [Coding]  
decode_syntax_element [Coding]  
decode_syntax_element_list [Coding]  
decode_term [Coding]  
decompose [Class] 
Compute a decomposition of a formula on a given class definition.

def_str [GDL]  
default_circle_structure [Structure] 
Return the default structure for the circle shape.

default_heuristic [Heuristic]  
default_heuristic_old [Heuristic]  
defs_of_rules [GDL]  
deg [OrderedPoly]  
del_elem [Structure] 
Remove the element
e and all incident relation tuples from struc .

del_elems [Structure] 
Remove elements
es and all incident relation tuples from
struc .

del_rel [Structure] 
Remove the tuple
tp from relation rn in structure struc .

del_rels [Structure] 
Remove the tuples
tps from relation rn in structure struc .

del_vars_quant [FormulaOps] 
Delete topmost quantification of
vs in the formula.

delete_dimacs_files [SatSolver] 
If false, dimacs files generated for external solvers will be preserved.

denominator_ratio [Rationals]  
diag_of_cnf [Diagram.S] 
Create a diagram from a CNF.

diag_of_qbf [Diagram] 
Make a diagram of a QBF.

diag_str [Diagram.S] 
Print a diagram as a formula.

diff [OrderedPoly]  
diff_elems [Structure] 
Elements from s1 which differ in s2, with differing relation names.

differentiate [OrderedPolySet] 
Differentiate all polynomials in the given set.

diffrels_struc [Structure] 
Differing relations (used in solver cache)

dimension [FormulaOps] 
Create a ndimensional formula for structures of given size.

dimension_vars [FormulaOps] 
Make the list of FO variable names ndimensional.

dimx [Picture]  
dimx [Matrix.MAT]  
dimx [Matrix]  
dimy [Picture]  
dimy [Matrix.MAT]  
dimy [Matrix]  
display_hterm [Coding] 
Convert a term to string concisely using the Greatest Lower Bound
notation.

display_sd [SyntaxDef]  
display_sd_bracketed [SyntaxDef]  
display_shortly_bracketed [Coding]  
display_super [Coding]  
display_term [Coding]  
display_term_bracketed [Coding]  
display_term_xml [Coding]  
distinguish [Distinguish] 
Find a formula holding on all
pos_strucs and on no neg_strucs .

distinguish_guess [Distinguish] 
Find a formula with at most
d1 unary and d2 binary definitions each with
k quantified variables holding on all pos_strucs and no neg_strucs .

distinguish_result_tc [Distinguish] 
Number of steps and base formula if distinguish returns a TC.

distinguish_upto [Distinguish] 
Find a
logic formula with at most qr quantifiers and k variables
which holds on all pos_strucs and on no neg_strucs .

div [OrderedPolySet] 
Compute factors r such that for some p,q in
ps,qs holds p = r*q.

div [OrderedPoly]  
div_big_int [Integers] 
Euclidean quotient of two big integers.

div_big_int_ratio [Rationals]  
div_int_ratio [Rationals]  
div_ratio [Rationals]  
div_ratio_big_int [Rationals]  
div_ratio_int [Rationals]  
div_rest [OrderedPoly]  
dnf [BoolFunction] 
Convert a function to DNF with eliminated quantifiers.

dnf_str [Sat] 
Return the given DNF formula as string.

E  
elem_name [Structure] 
The element name of an element (given by integers)

elem_nbr [Structure] 
The integer corresponding to a given element name.

elem_str [ParseArc] 
Print a parser elem.

elem_str [Structure] 
Print the elements
e as string.

elements [OrderedPolySet]  
elements [Structure] 
Return the list of elements in a structure.

elems [Structure] 
Return the set of elements in a structure.

elems_of_list [Structure]  
elems_with_val [Structure] 
Return the elements on which function
f has value x in struc .

elim_bounded [Diagram.S] 
Top variable elimination until size, else branch elimination.

elim_bounded_sat [Diagram.S] 
Sat check based on elim_bounded.

elim_ground_distinct [GDL]  
elim_pattern_args [GDL] 
Eliminate arguments of relations that are defined by nonwildcard
pattern matching (i.e.

elim_sat [Diagram.S] 
Sat check by repeated top variable elimination.

elim_top_until [Diagram.S] 
Eliminate the top variable recursively up to the given size.

elim_var [Diagram.S] 
Eliminate an existential variable (or universal, if set).

elt_of_int [Matrix.MAT]  
empty [OrderedPolySet]  
empty [Bitvector] 
Empty bit vector.

empty_gdl_translation [TranslateGame]  
empty_isbs [Term]  
empty_path_set [GDL]  
empty_rrules [Rewriting]  
empty_rule [DiscreteRule] 
Empty rule.

empty_s_isb [Term]  
empty_s_sb [Term] 
Operations on substitutions.

empty_sbs [Term] 
Find a term corresponding to the name of a variable or raise
Not_found .

empty_state [Arena]  
empty_structure [Structure] 
Return the empty structure (with empty signature).

empty_t_isb [Term]  
empty_t_sb [Term]  
empty_transl_data [TranslateFormula]  
empty_with_signat [Structure] 
Return the empty structure with given relational signature.

enumerate_matchings [DiscreteRule] 
Enumerate matchings returned by
DiscreteRule.find_matchings for the same
structure and rewrite rule.

eps_path_set [GDL] 
Add path to a set.

eq_big_int [Integers]  
eq_big_int_ratio [Rationals]  
eq_bool_name [BuiltinLang]  
eq_ratio [Rationals]  
eq_str [Formula]  
equal [Term.HashableTerm]  
equal [OrderedPoly]  
equal [Structure]  
equal_for_rewriting [Term]  
equal_mod_tvars [Term] 
Check for equality but ignore RHS subterms corresponding to LHS
type variables.

equal_state [Arena]  
equal_vars [Assignments] 
Enforce that in
aset the variable u is equal to w .

equational_def_style [Arena] 
Whether to print relation definitions as equations, or using the C
syntax.

error_when_null_denominator_flag [MiscNum]  
eval_counter [Solver] 
Counter of internal formula evaluations for profiling.

evaluate [Solver.M] 
Evaluate the formula on the structure.

evaluate_partial [Solver.M] 
Evaluate the formula on the structure and join with given assignment.

evaluate_real [Solver.M] 
Evaluate real expressions.

exception_name [BuiltinLang]  
expand_definitions [GDL] 
Expand branches of a definition inlining the provided
definitions.

expand_formula [FormulaSubst] 
Expand Let's and RLet's in formula.

expand_players [GDL]  
expand_real_expr [FormulaSubst]  
expanded_description [Heuristic] 
Returns a disjunction of existentially quantified conjunctions of
atoms each disjunct being equivalent to the given formula in the
given model.

expanded_form [Heuristic] 
Apply a variant of
Heuristic.expanded_description to subformulas for
which it succeeds.

ext_str [Structure] 
Print the structure
struc as string, in extensive form (not using
condensed representations like boards).

extend_arc_list [ParseArc] 
Extends all the arcs in the given list that can be extended
and removes all other arcs.

extract [Aux.PRIOQUEUE]  
F  
f_signature [Structure] 
Return the list of functions.

ff_tnf [FFTNF] 
FF Type Normal Form: a variant of Type Normal Form that promotes
literals with older (earlier quantified) variables, and if
undecisive, according to the given relation.

ffsep [FFTNF]  
filter_possibly_redundant [TranslateGame] 
When
filter_possibly_redundant is false, only whole groups of
variablesharing "next" clause literals that together are subsumed
by "legal" clause literals are filtered out.

find [Term.TermHashtbl]  
find_all [Term.TermHashtbl]  
find_cycle [GDL]  
find_elem [Structure]  
find_example [Reduction] 
Find an example structure of a given size for a formula.

find_index [Aux] 
Find the index of the first occurrence of a value in a list,
counting from zero.

find_lfp_iter [Lfp] 
Find lfp formula iterating on counterexaples.

find_matchings [DiscreteRule] 
Find all embeddings of a rule.

find_model_qbf [QBF] 
Find a model for a QBF formula.

find_model_qbf_qf [QBF] 
Find a model for a quantifier free QBF formula.

find_or_new_elem [Structure] 
Find an element in the structure, and if not present, add new one.

find_reduct [Reduction] 
Find reduction from
cfrom to cto of dimension dim , correct upto
size size and with at most nbr_cl clauses.

find_reduct_iter [Reduction] 
Find reduction iterating on counterexamples.

find_reduct_iter_counterexample [Reduction] 
Return the current counterexample structure.

find_reduct_iter_start [Reduction] 
Find reduction iterating on counterexaples as above  start

find_reduct_iter_step [Reduction] 
Find reduction iterating on counterexaples as above  step

find_rel_arg [GDL]  
find_so [Solver] 
Find assignment for secondorder variables and add it to the structure.

find_some [Aux]  
find_try [Aux] 
Find the first element of the list on which the function does not
raise
Not_found and return its result.

flat_grammar_of_sd_list [SyntaxDef]  
flatten [BoolFunction] 
Flatten conjunctions and disjunctions.

flatten [Formula] 
Only flatten the formula.

flatten_qbf [QBF] 
Helper function to flatten multiple or's, and's, and quantifiers.

flatten_re [Formula]  
flatten_sort [Formula] 
Flatten and sort multiple or's and and's.

flatten_sort_re [Formula]  
flip [Picture] 
Flip a picture.

float_of_big_int [Integers] 
Returns a floatingpoint number approximating the given big integer.

float_of_num [Numbers]  
float_of_ratio [Rationals]  
floating_precision [MiscNum]  
floor_ratio [Rationals]  
fluent_preconds [DiscreteRule] 
A fluent precondition is an approximation to the condition on a
structure for the positive/negative fluent to appear/disappear at a
position.

fluents [DiscreteRule] 
Fluents are relations that are changed by rules.

fluents_heuristic [Heuristic]  
fluents_make [DiscreteRule]  
fn_apply [Term]  
fo_assgn_of_list [Assignments] 
Convert an association list into an assignment for FO variables.

fo_assgn_to_list [Assignments] 
Convert the FO part of an assingment set into a list of substitutions.

fo_tc_param [FormulaSubst] 
Parameter governing whether to use LFP or FO TC when parsing.

fo_var_of_string [Formula]  
fold [Matrix.MAT]  
fold [Term.TermHashtbl]  
fold_formula [FormulaMap] 
Fold the structure using the operations.

fold_left_try [Aux] 
Fold
f over the list collecting results whose computation does
not raise Not_found .

fold_mat [Matrix]  
fold_n [Aux] 
Iterate a function
n times: f^n(x) .

fold_over_atoms [FormulaMap]  
fold_over_formulas [Arena]  
fold_over_formulas [ContinuousRule]  
fold_over_formulas [DiscreteRule]  
fold_over_formulas_expr [FormulaMap]  
fold_over_literals [FormulaMap]  
fold_real_expr [FormulaMap]  
fold_rect [Matrix]  
force_competitive [Heuristic] 
Irrespective of the shape of payoffs, take the difference of
heuristics as the final heuristic for each player (in
Heuristic.default_heuristic_old ).

force_order [QBF] 
Variable ordering heuristiv called FORCE, a centerofgravity positioning
based simulation of MINCE, from the paper by Aloul, Markov and Sakallah.

formula [Diagram.S]  
formula_to_cnf [QBF] 
Convert an arbitrary formula to CNF via Boolean combinations.

fprint [ContinuousRule]  
fprint [Structure]  
fprint [BoolFunction]  
fprint [Formula]  
fprint_def [BoolFunction]  
fprint_defs [BoolFunction]  
fprint_eqs [Formula] 
Print an equation system.

fprint_ext_structure [Structure]  
fprint_full [ContinuousRule]  
fprint_full [DiscreteRule]  
fprint_fun [Structure]  
fprint_ppm [Picture] 
Print a picture in the simple PPM format to a formatter.

fprint_prec [Formula]  
fprint_real [Formula]  
fprint_real_prec [Formula]  
fprint_rel [Structure] 
Print the relation with tuples
ts .

fprint_rule [DiscreteRule]  
fprint_sep_list [Aux] 
Print an unboxed separated list, with breaks after the separator.

fprint_state [Arena]  
fprint_state_full [Arena]  
free_for_rel [Structure] 
Return a structure with a single relation of given arity, over a
single tuple, of different elements.

free_vars [QBF] 
Free variables in a QBF.

free_vars [FormulaSubst] 
Free variables in a formula.

free_vars_hash [QBF] 
Add free variables of a QBF to the given hash table.

fst3 [Aux]  
full_join_rel [Assignments]  
fun_definition_cons_name [BuiltinLang]  
fun_definition_name [BuiltinLang]  
fun_definition_tp [BuiltinLang]  
fun_type_name [Term] 
The name for function type (type of unapplied function term).

fun_val [Structure] 
Return the value of function
f on e in struc .

func_graph [GDL]  
func_sd_of_sd [Coding]  
functions [Structure] 
Functions in the structure.

G  
game_move_str [Arena]  
gaussian [Picture]  
gc_elems [Structure] 
Remove the elements that are not incident to any relation (and have
no defined properties, unless
ignore_funs is given).

gcd_big_int [Integers] 
Greatest common divisor of two big integers.

gcd_int [MiscNum]  
gdl_rel_graph [GDL] 
Saturation currently exposed for testing purposes.

gdl_rule_str [GDL]  
gdl_rules_str [GDL]  
ge_big_int [Integers]  
generate_test_case [TranslateGame]  
get [Diagram.S] 
Export to unordered generic type.

get_atoms [FormulaMap] 
All atoms in a formula.

get_bit [Bitvector] 
Get the bit at the given position.

get_decl [Term]  
get_h1 [HashCons.S] 
Get a managed (data, data) cache.

get_h1_alpha [HashCons.S] 
Get a managed (data, 'a) cache.

get_h2 [HashCons.S] 
Get a managed (data * data, data) cache.

get_hv [HashCons.S] 
Get a managed (data * data, other_value) cache.

get_nonvar_definitions_name [BuiltinLang]  
get_real_val [Solver.M] 
Get the value of a real expression without free variables.

get_relations_constants [FormulaMap] 
All relations in a formula, with arities, and constants that appear.

get_solver [SatSolver]  
get_subclasses [Term]  
get_superclasses [Term]  
get_t_pos [Term]  
glb [Term] 
Greatest Lower Bound Unification w.r.t.

glb_name [BuiltinLang]  
global_sdefs [BuiltinLang] 
Builtin syntax definitions to introduce when building a TRS.

graph_mem [GDL]  
graph_to_atoms [GDL]  
ground_rewrite_rule_cons_name [BuiltinLang]  
ground_vars_at_paths [GDL]  ground_vars_at_paths prepare_lits ps_sterms clauses expands
subterms that have occurrences at paths in ps_sterms in some
state term of a clause (from which preprocessed literals are
extracted by prepare_lits ), by substituting their variables with
corresponding subterms of terms provided in ps_sterms .

gt_big_int [Integers] 
Usual boolean comparisons between two big integers.

guard_tuple_str [Distinguish] 
Print a guard tuple, as returned above, to string.

guarded_type [Distinguish] 
Guarded
?existential qr type in length of tuple variables
of tuple in struc .

guarded_types [Distinguish] 
All guarded
?existential types of rank qr of
guarded k tuples in struc .

guards [Distinguish] 
Generate all guarded substitutions of
tuple with the guards.

H  
has_quantifiers [QBF] 
Check if a qbf has quantifiers inside.

has_s_var [Term]  
has_t_var [Term]  
hash [Term.HashableTerm]  
hash [Diagram.Variables]  
hashSIZE [Diagram] 
Hash size used when making the module.

hash_list [HashCons] 
A hashing function for 'a hc lists.

hashcons [HashCons.S] 
Hashcons a value.

hc [Formula] 
Hashcons a formula.

hc_real [Formula] 
Hashcons a real expression.

head_grounding [Term] 
Identity on nonvariable terms, return type of sharing variable
and upper bound of type variable.

hlist_cons_name [BuiltinLang]  
hlist_empty_name [BuiltinLang]  
hlist_name [BuiltinLang]  
hlist_one_name [BuiltinLang]  
hlist_tp [BuiltinLang]  
I  
identity_map [FormulaMap] 
Identity map to be refined using the
with syntax.

if_then_else_name [BuiltinLang]  
if_then_else_rules [Coding]  
image [Picture] 
Fill the RGB channels from floats in range 0..1.

in_bounds [Matrix]  
incident [Structure] 
Return the list of relation tuples incident to an element
e in struc .

init [Matrix.MAT] 
Maps from an array to another array of possibly different
type.

init [GameTree] 
Game tree initialization.

init_abstract [GameTree] 
Abstract initialization function.

init_mat [Matrix]  
inline_defs [BoolFunction] 
Inline all nonfixedpoint definitions.

input_rewrite_rule_name [BuiltinLang]  
input_rewrite_rule_tp [BuiltinLang]  
insert [Aux.PRIOQUEUE]  
insert_nth [Aux] 
Insert as
n th element of a list (counting from zero).

int_case_str [SignTable] 
Print a case, i.e.

int_of_big_int [Integers] 
Convert a big integer to a small integer (type
int ).

int_of_num [Numbers]  
int_of_ratio [Rationals]  
int_pow [Aux]  
int_to_bits [Coding]  
integer_of_level [BuiltinLang] 
Remove level prefixes and indicators from the head of the term.

integer_ratio [Rationals]  
intmap_filter [Aux]  
intmap_of_assoc [Aux]  
ints_of_list [Aux]  
inv_names [Structure] 
The inverse map of element names.

is_alpha_identity [DiscreteRule]  
is_alphanum [Aux]  
is_atom [Formula]  
is_const [Formula] 
Check variable type.

is_constant_sum [Heuristic]  
is_constant_sum_one [Heuristic]  
is_digit [Aux]  
is_eliminated [SatSolver.S]  
is_empty [Bitvector] 
Check if a bitvector is empty.

is_empty [Aux.PRIOQUEUE]  
is_fo [Formula]  
is_int_big_int [Integers] 
Test whether the given big integer is small enough to
be representable as a small integer (type
int )
without loss of precision.

is_integer_num [Numbers] 
Is the number an integer?

is_integer_ratio [Rationals]  
is_letter [Aux]  
is_level_ind_name [BuiltinLang]  
is_level_name [BuiltinLang]  
is_literal [Formula]  
is_lowercase [Aux]  
is_pos [Diagram.Variables]  
is_real [Formula]  
is_right [Aux]  
is_sat [Sat] 
Check satisfiability of a formula in CNF, return just true or false.

is_so [Formula]  
is_space [Aux]  
is_superclass_of [Term] 
A very quick check that ignores all subterms, if a term is a
superclass of another term (or the same class).

is_turnbased [TranslateGame]  
is_uppercase [Aux] 
Character classes.

is_zero [OrderedPoly]  
isa_match [Term] 
Returns the ISAmatching or raises
UNIFY .

isa_unify [Term] 
Returns the ISAunification: like ISAmatching, but does not treat
the RHS type variables as constants, instead infers their upper
bounds.

isubsts_fstr [Term]  
isubsts_map [Term]  
isubsts_str [Term]  
iter [Matrix.MAT]  
iter [Term.TermHashtbl]  
iter [OrderedPolySet]  
iter_mat [Matrix]  
iter_vars [QBF] 
Iterate given function on all variables of the qbf.

J  
join [Assignments] 
This function joins two assignment sets, i.e.

join_rel [Assignments]  
join_sign_ops [SignTable] 
Given two sign_ops
x and y return a sign op for "x and y".

L  
label_str [Arena] 
Print a label as a string.

last_no_parse_message [ParseArc]  
latest_unfold_iters_left [Play] 
In case the computation is interrupted by a timeout, how many
iterations were left to perform by
Play.maximax_unfold_choose
or Play.unfold_maximax_upto .

le_big_int [Integers]  
leading_coeff [OrderedPolySet] 
Extract leading coefficients from all polynomials in the set.

leading_coeff [OrderedPoly]  
learnFromParties [LearnGame] 
Learn a twoplayer winloseortie game given 4 sets of plays of another
game
source : wins0 which are now supposed to be won by Player 0,
wins1  now won by Player 1, tie  now a tie, and wrong which
are not correct plays of the newly constructed game.

least_int [MiscNum]  
length [Term.TermHashtbl]  
length_of_int [MiscNum]  
let_be_name [BuiltinLang]  
let_ground_be_name [BuiltinLang]  
let_major_be_name [BuiltinLang]  
let_major_ground_be_name [BuiltinLang]  
level_A_i_name [BuiltinLang]  
level_A_name [BuiltinLang]  
level_A_pref [BuiltinLang]  
level_B_i_name [BuiltinLang]  
level_B_name [BuiltinLang]  
level_B_pref [BuiltinLang]  
level_C_i_name [BuiltinLang]  
level_C_name [BuiltinLang]  
level_C_pref [BuiltinLang]  
level_D_i_name [BuiltinLang]  
level_D_name [BuiltinLang]  
level_D_pref [BuiltinLang]  
level_E_i_name [BuiltinLang]  
level_E_name [BuiltinLang]  
level_E_pref [BuiltinLang]  
lfp_outline [Lfp] 
Outline with definitions of the form "U_i(x)=+/basic_outline k_i c_i",
given
a_i, k_i, c_i , and combined to lfp U(x_a) = +/ basic neg k c.

lhs [ContinuousRule]  
list_cons_name [BuiltinLang]  
list_cons_sd [BuiltinLang]  
list_diff [Aux] 
Set difference:
List.filter (fun e > not (List.mem e b)) a .

list_find_all_max [Aux] 
Find all maximal elements in a list.

list_fprint [Aux] 
Printf helper functions.

list_init [Aux] 
Create a list of given length initialized from the indices.

list_inter [Aux] 
Intersection:
list_inter a b = List.filter (fun e > List.mem e b) a .

list_moves [Arena] 
Get moves and resulting game states for all rules the players can apply
in the given game state.

list_moves_shifts [Arena] 
As
list_moves but with animation shifts for each move.

list_nil_name [BuiltinLang]  
list_nil_sd [BuiltinLang]  
list_of_opt [Aux]  
list_remove [Aux] 
Remove all elements equal to the argument, using structural equality.

list_rev_split [Aux] 
Tailrecursive List.split with accumulators; reverses the lists.

list_sd [BuiltinLang]  
list_to_set_list [Assignments]  
list_tp [BuiltinLang]  
list_tp_a [BuiltinLang]  
list_tp_name [BuiltinLang]  
literal_str [GDL]  
literals_str [GDL]  
literals_vars [GDL]  
load_file_name [BuiltinLang]  
log [Diagram.S] 
Log a variable, diagram and variable assignment.

log_no_cases [SignTable] 
Estimate the (base3) logarithm of the number of cases needed for
pset .

lookahead [SatSolver.S]  
lower [OrderedPoly]  
lt_big_int [Integers]  
lub [Term] 
Least Upper Bound Unification w.r.t.

M  
make_empty [Aux.PRIOQUEUE]  
make_fo_tc_conj [FormulaSubst] 
Firstorder
k step refl.

make_fo_tc_disj [FormulaSubst]  
make_fold [FormulaMap]  
make_fp_inductive [FormulaOps] 
Replace fixedpoints by their inductive evaluation for given size.

make_layer [QBF] 
Make a layer of a convolutional network with k maps.

make_lfp_tc [FormulaSubst] 
Transitive closure of phi(x, y, z) over x and y, an LFP formula.

make_location [Arena]  
make_move [Arena] 
Make a move in a game.

make_move_arena [Arena]  
make_mso_tc [FormulaSubst] 
Transitive closure of phi(x, y, z) over x and y, an MSO formula.

make_ordered [Poly] 
Make an ordered polynomial from
p with prio_list order on variables,i.e.

make_ordered_list [Poly] 
Make ordered polynomials from
ps with prio_list order on variables.

make_ordered_pair_list [Poly] 
Make ordered polynomials from first components of
ps , prio_list order.

make_rule [ContinuousRule] 
Create a continuous rule given a named discrete rule and other params.

make_standard_tc [FormulaSubst] 
The default TC syntax: LFP if fo_tc_param = 0 else FO with fo_tc_param.

make_unordered [Poly]  
make_unordered_pair_list [Poly]  
make_xml_compatible [SyntaxDef]  
map [Matrix.MAT]  
map [OrderedPolySet] 
Maps a function to all polynomials in the set.

map [Aux.PRIOQUEUE]  
map_choice [Aux]  
map_constants [Heuristic] 
Rewrite numeric constants inside an expression.

map_formula [FormulaMap] 
Map through the structure adjusting subformulas/subexpressions.

map_fst [Aux]  
map_mat [Matrix]  
map_option [Aux] 
Map optional value, with a default result for the
None case.

map_paths [GDL] 
Find the list of results of a function applied to paths from the
given set that are in the term, and to subterms at these paths.

map_prepend [Aux] 
Map a second list and prepend the result to the first list, by
single traversal.

map_real_expr [FormulaMap]  
map_reduce [Aux] 
Map elements into keyvalue pairs, and fold values with the same
key.

map_rev_prepend [Aux]  
map_snd [Aux]  
map_some [Aux] 
Map a list filtering out some elements.

map_to_all_vars [FormulaMap] 
Map

map_to_atoms [FormulaMap]  
map_to_atoms_expr [FormulaMap]  
map_to_atoms_full [FormulaMap] 
Map
f to all atoms in the given formula.

map_to_atoms_full_re [FormulaMap]  
map_to_discrete [Arena] 
Map to the structure representation of discrete part of rules.

map_to_formulas [Arena]  
map_to_formulas [ContinuousRule]  
map_to_formulas [DiscreteRule] 
Map and fold over formulas in a rule.

map_to_formulas_expr [FormulaMap] 
Map
f to toplevel formulas in the real expression (Char s and
Sum guards).

map_to_literals [FormulaMap] 
Map
f to all literals (i.e.

map_to_literals_expr [FormulaMap]  
map_to_structures [Arena]  
map_to_structures [DiscreteRule]  
map_try [Aux] 
Map
f on the list collecting results whose computation does not
raise Not_found .

mask_blank [GDL]  
match_nonblank [GDL] 
Check for equality modulo ground terms on the right.

matches [ContinuousRule] 
Find all matches of
r in struc which satisfy r 's precondition.

matches [Coding] 
Application of term substitutions (only flat functional
substitutes).

matches_post [ContinuousRule] 
Matches which satisfy postcondition with time 1 and empty params

matching_of_names [Arena] 
Translate from names to elements to get rule embedding.

matching_str [ContinuousRule]  
matching_str [DiscreteRule] 
Printing.

max [Diagram.Variables]  
max_big_int [Integers] 
Return the greater of its two arguments.

max_power10_int [MiscNum]  
max_var [QBF] 
Maximal variable number occuring (positively or negatively) in phi.

maximal [Aux] 
Return the list of all maximal elements, under the given lessorequal
comparison.

maximal_o [Aux] 
Return single maximal element (in case of "less" or
"lessorequal" comparison) .

maximal_unique [Aux] 
Return the list of all maximal elements, under the given lessorequal
comparison.

maximax_unfold_choose [Play] 
Maximax unfold upto iterations and choose move.

maxpool [QBF] 
Maxpool a XxY bitimage to a (X/2)x(Y/2) bitimage.

mem [Term.TermHashtbl]  
mem_rev_assoc [Aux] 
Check if the value is associated with a key in the keyvalue pairs,
using structural equality.

merge [Aux] 
Merging of two lists, sorts arguments and produces a
cmp sorted list.

merge_graphs [GDL]  
merge_rules [Rewriting]  
merge_terms [GDL] 
The set of paths that merges two terms, the cardinality of this
set, and the size of the largest common subtree.

message_for_term [TRS]  
mgu_iter [Term] 
Iterated Substitution based variant of the Most General Unifier
substitution, throws
UNIFY if not unifiable.

min_big_int [Integers] 
Return the smaller of its two arguments.

min_type_omitting [Distinguish] 
Find the minimal
logic type of struc not included in neg_types
and with at most qr quantifiers and k variables.

minimize [Sat] 
Greedy minimize the number of between
sep positive variables in a model.

mintp [FormulaOps] 
Minimal type satisfying f over rels extending vars.

minus_big_int [Integers] 
Unary negation.

minus_ratio [Rationals]  
mix_heur [Heuristic] 
Various constructed heuristics.

mixed_sat [Diagram.S]  
mk_and [Diagram.S] 
Conjunction of two diagrams.

mk_or [Diagram.S] 
Disjunction of two diagrams.

mod_big_int [Integers] 
Euclidean modulus of two big integers.

mod_num [Numbers] 
Euclidean division: remainder.

model_val [Structure] 
Return the model assigned by
f to e in struc .

modified_remainder [OrderedPolySet] 
Compute the modified remainder for all pairs of polynomials p from
ps1 and q!=p from qs1 such that the degree of p >= degree of q.

modified_remainder [OrderedPoly]  
mona_str [Formula]  
monochrome [Picture]  
monster_int [MiscNum]  
move_str [Arena] 
Print a game as a string.

mul [OrderedPoly]  
mult_big_int [Integers] 
Multiplication of two big integers.

mult_big_int_ratio [Rationals]  
mult_int_big_int [Integers] 
Multiplication of a big integer by a small integer

mult_int_ratio [Rationals]  
mult_ratio [Rationals]  
multiple [OrderedPoly]  
multiple_num [OrderedPoly]  
N  
name_of_sd [SyntaxDef]  
named_str [Assignments] 
Print the given assignment as string, using element names.

names [Structure] 
The map containing element names.

nat_of_big_int [Integers]  
nbits [QBF] 
How many bits to use in numbers or conjunctions in gates.

nbr_elems [Structure] 
Number of elements in a structure.

nbr_set_bits [Bitvector] 
Number of bits set in a vector.

needs_brackets [BuiltinLang]  
neg [OrderedPoly]  
neg [Diagram.Variables]  
neg [Aux]  neg f x = not (f x)

neg_lit [SatSolver.S]  
neg_sign_op [SignTable] 
Negate a sign_op.

negate_bodies [GDL] 
Form clause bodies whose disjunction is equivalent to the
negation of disjunction of given clause bodies.

new_rules_set [Rewriting] 
A new set of rewriting rules, containing the given list

new_var [SatSolver.S]  
niceness [GameSimpl]  
nnf [FormulaOps] 
Convert formula to NNF and additionally negate if
neg is set.

nnf [QBF] 
Convert a QBF to NNF and additionally negate if
neg is set.

nnf_dnf [GDL]  
no_external [QBF] 
Upto this clause number we don't use external solvers (default: 4).

no_root_predicates [TranslateFormula] 
Whether to add root predicates.

node_info [GameTree] 
Get the stored information of a game tree node.

node_values [GameTree] 
The values of a game tree node.

noop_move [TranslateGame]  
normalise [Rewriting] 
Normalise the Term.

normalise_brackets [Rewriting] 
Just normalise the special bracketing function.

normalise_with_sys [TRS]  
normalize [Picture] 
Normalize

normalize_ratio [Rationals]  
normalize_ratio_flag [MiscNum]  
normalize_spaces [Aux] 
Replace all white space sequences by a simple space, strip on both ends.

not_conflicting_name [Aux] 
Returns a string prolonging
s and not appearing in names .

not_conflicting_names [Aux] 
Returns
n strings proloning s and not appearing in names .

not_unique [Aux] 
Check whether the list contains duplicates, using structural equality.

ntype [Distinguish] 
The
?existential qr type in length of tuple variables
of tuple in struc .

ntypes [Distinguish] 
All
?existential types of rank qr of all k tuples in struc .

null_denominator [Rationals]  
num_bits_int [MiscNum]  
num_digits_big_int [Integers] 
Return the number of machine words used to store the
given big integer.

num_of_int [Numbers]  
num_of_string [Numbers]  
numerator_ratio [Rationals]  
O  
of_list [Bitvector] 
Mark the bits at positions given in the list.

of_list [Aux.PRIOQUEUE]  
of_payoff [Heuristic] 
Heuristic of payoff expression.

omap [Aux]  
omit_leading [OrderedPolySet] 
Omit leading coefficients from all polynomials in the given set.

omit_leading [OrderedPoly]  
optimize_goal [GDL]  
optimize_program [GDL]  
orig_rel_of [DiscreteRule]  
our_turn [TranslateGame]  
P  
p_pn_nnf [FFTNF] 
Prenexnormal negation normal form of a formula with minimized
alternation and preference to start from existential quantification.

pairs [Aux] 
A list of all pairs of elements that preserve the order of
elements from the list.

parallel_toss [GameTree] 
We can parallelize computation to a second running Toss client.

parse [ParseArc]  
parse_board [Structure] 
Parse a rectangular board as a model, using "R" for rows, "C" for
columns, and the letter at a position for a unary
predicate.

parse_class [ClassParser]  
parse_disambiguate_with_sys [TRS]  
parse_discrete_rule [ArenaParser]  
parse_discrete_rule [ContinuousRuleParser]  
parse_discrete_rule [DiscreteRuleParser]  
parse_expr_eqs [ArenaParser]  
parse_expr_eqs [ContinuousRuleParser]  
parse_expr_eqs [DiscreteRuleParser]  
parse_expr_eqs [ClassParser]  
parse_expr_eqs [StructureParser]  
parse_expr_eqs [FormulaParser]  
parse_formula [ArenaParser]  
parse_formula [ContinuousRuleParser]  
parse_formula [DiscreteRuleParser]  
parse_formula [ClassParser]  
parse_formula [RealQuantElimParser]  
parse_formula [StructureParser]  
parse_formula [FormulaParser]  
parse_game_defs [ArenaParser]  
parse_game_description [GDLParser]  
parse_game_state [ArenaParser]  
parse_literal_list [GDLParser]  
parse_real_expr [ArenaParser]  
parse_real_expr [ContinuousRuleParser]  
parse_real_expr [DiscreteRuleParser]  
parse_real_expr [ClassParser]  
parse_real_expr [StructureParser]  
parse_real_expr [FormulaParser]  
parse_reduct [Reduction] 
Parse a reduction.

parse_rel_const_defs [ArenaParser]  
parse_rel_const_defs [ContinuousRuleParser]  
parse_rel_const_defs [DiscreteRuleParser]  
parse_rel_const_defs [ClassParser]  
parse_rel_const_defs [StructureParser]  
parse_rel_defs [ArenaParser]  
parse_rel_defs [ContinuousRuleParser]  
parse_rel_defs [DiscreteRuleParser]  
parse_rel_defs [ClassParser]  
parse_rel_defs [StructureParser]  
parse_request [GDLParser]  
parse_rule [ArenaParser]  
parse_rule [ContinuousRuleParser]  
parse_structure [ArenaParser]  
parse_structure [ContinuousRuleParser]  
parse_structure [DiscreteRuleParser]  
parse_structure [ClassParser]  
parse_structure [StructureParser]  
parse_term [GDLParser]  
parse_term [Coding]  
parse_to_array [ParseArc]  
parse_with_sdefs [ParseArc]  
parse_with_sys [TRS]  
parsed_tvar_b_name [BuiltinLang]  
parsed_tvar_name [BuiltinLang]  
parsed_tvar_tp [BuiltinLang]  
parsimony_threshold_1 [FFTNF]  
parsimony_threshold_2 [FFTNF]  
parsing_postprocess [ParseArc]  
partition_choice [Aux] 
Partition a list of tagged elements into the
Left and
Right tagged elements.

partition_map [Aux] 
Map elements and partition them according to
Aux.choice tags (see
also Aux.partition_choice ).

path_file_name [BuiltinLang]  
path_library_name [BuiltinLang]  
path_str [GDL]  
paths_intersect [GDL]  
paths_to_list [GDL] 
List the paths in a set.

paths_union [GDL]  
peek [Aux.PRIOQUEUE]  
pi [Aux]  
piecewise_linear [FormulaOps] 
Generate a piecewiselinear function of a given argument from a
graph.

player [GameTree] 
Player in the given node.

playout_fixpoint [GDL]  
playout_horizon [TranslateGame] 
Limit on plys for both aggregate and random playouts.

playout_prolog [GDL]  
playout_satur [GDL] 
Besides the aggregate or random playout, also return the
separation of rules into static and dynamic.

playouts_for_rule_filtering [TranslateGame] 
How many random playouts to generate states for rule filtering (a
rule needs to match in at least one generated state to be kept).

pnf [FormulaOps] 
Prenex normal form.

poly_sign_op_cmp [SignTable]  
pop_assoc [Aux] 
Find the value associated with the first occurrence of the key and
remove them from the list.

pop_assq [Aux] 
As
Aux.pop_assoc , but uses physical equality.

pop_find [Aux] 
Find an element satisfying the predicate and separate it from the list.

pos_lit [SatSolver.S]  
pos_state_terms [GDL]  
position_str [Term]  
pow [Poly] 
Power function used in parser.

pow [OrderedPoly]  
power [Aux]  power dom img generates all functions with domain dom and
image img , as graphs.

pred_on_path_subterm [GDL] 
Some Toss predicates are generated from a path and an expected
subterm at that path.

predicates_partition [Distinguish] 
If set, predicates paritition the universe (are disjoint and total).

preprocess_program [GDL]  
pretty_print_sd [Coding]  
print [ContinuousRule]  
print [Structure]  
print [BoolFunction] 
Print.

print [Formula]  
print_cqbf [QBF] 
Print a QBF formula in cqbf format.

print_def [BoolFunction] 
Print definition.

print_defs [BoolFunction] 
Print definitions.

print_dimacs [QBF] 
Print dimacs for a cnf.

print_grammar [SyntaxDef]  
print_heur [Heuristic] 
Simple heuristic print helper.

print_lparse [QBF] 
Print a 2QBF formula in lparse format.

print_qdimacs [QBF] 
Print a QBF formula in qdimacs format.

print_qiscas [QBF] 
Print a QBF formula in qiscas format.

print_qpro [QBF] 
Print a QBF formula in qpro format.

print_real [Formula]  
print_reduct_find [Reduction] 
Print reductionfinding condition in qpro (fmt=0), lp (fmt=1),or qdimacs.

print_rule [DiscreteRule]  
print_state [Arena]  
print_xslt [SyntaxDef]  
priority_input_rewrite_rule_name [BuiltinLang]  
priority_input_rewrite_rule_tp [BuiltinLang]  
process_definition [Arena] 
Create a game state, possibly by extending an old state, from a
list of definitions (usually corresponding to a ".toss" file.)

process_with_system [TRS]  
product [Aux] 
Cartesian product of lists.

product_size [Aux] 
Size of the cartesian product of lists; max_int if the size is bigger.

program_clauses [GDL]  
project [Assignments] 
Project assignments on a given variable.

project_list [Assignments] 
Projection on a list of variables.

promote_rels [FFTNF] 
Promote relations from the given set.

propagate [Diagram.S] 
Fixedpoint of propagate_once.

propagate_once [Diagram.S] 
Propagate variables and all other singletons.

prune_indef_vars [DiscreteRule]  
prune_unused_quants [FormulaOps] 
Remove quantifiers that bind only variables not occurring freely
in the body.

push_quant [FormulaSubst] 
Basic pushing of quantifiers inside a formula

put_space [SyntaxDef]  
Q  
qbf_hc [QBF] 
Hashcons a raw QBF formula.

qbf_of_bf [QBF] 
Convert a boolean formula to QBF.

qbf_str [QBF] 
Print a QBF formula.

quantified_vars [FormulaSubst] 
Quantified variables in a formula.

quo_num [Numbers] 
Euclidean division: quotient.

quomod_big_int [Integers] 
Euclidean division of two big integers.

R  
random_elem [Aux] 
Random element of a list.

range [FormulaSubst] 
Rough estimate of the range of a realvalued expression given structure
size and function, realvariable value and predicate size estimates.

range [Aux] 
Returns an int list from
from (default 0) to k1.

ratio_of_big_int [Rationals]  
ratio_of_int [Rationals]  
ratio_of_string [Rationals]  
read_pic [Picture] 
Read a picture from a scanning buffer.

read_ppm [QBF] 
Read a PPM grayscale image into a list of 8 bitmatrices.

read_qdimacs [QBF] 
Read a qdimacs description of a QBF from a string.

real_str [Formula] 
Print a real_expr as a string.

real_var_of_string [Formula]  
refine_leaf_paths [GDL] 
If some path points only to bigger than one (i.e.

refine_paths_avoiding [GDL]  refine_paths_avoiding paths avoid_later avoid_now terms splits
paths in the set until, if possible, none of subterms at the paths
meets the predicate avoid_later ; it does not descend subterms
for which avoid_now holds.

regcolors [Picture] 
Average colors per region.

regions [Picture] 
Compute edgeseparated regions, region numbers start from 1,
remaining edges are pseudoregion 0.

register_dnf_param [Solver] 
Parameter for dnf conversion in registration.

rel_atom_str [GDL]  
rel_atoms_str [GDL]  
rel_graph [Structure] 
Graph of a relation in a model, returns an empty set if the
relation is not in the signature.

rel_incidence [Structure] 
Incidences of a relation in a model, returns an empty set if the
relation is not in the signature.

rel_of_atom [GDL]  
rel_on_paths [GDL] 
Toss relations hold between subterms of GDL state terms: generate
Toss relation name.

rel_signature [Structure] 
Return the list of relations with their arities.

rel_size [Structure] 
Size of a relation, i.e.

rel_sizes [Structure] 
Cardinality of graphs of all relations in the structure.

rel_str [Structure] 
Print the relation named
rel_name with tuples ts as string.

relations [Structure] 
Relations in the structure.

rels_signs [FormulaOps] 
Find all positively and negatively occurring relations.

rels_signs_expr [FormulaOps]  
rels_unify [GDL]  
remove [Term.TermHashtbl]  
remove [Diagram.S] 
Remove all occurences of the given variable, whatever they mean.

remove_exist [GameSimpl]  
remove_last [Aux] 
Remove the last element in a list; raise Not_found for [].

remove_one [Aux] 
Remove an occurrence of a value (uses structural equality).

remove_redundant [FormulaOps] 
Simplify the formula by removing relational literals, depending on
what literals they are conjoined with up the tree, whether they are
in a disjunction and what literals they are disjoined with, keeping
track of the sign (variance) of a position.

remove_sharing [BuiltinLang]  
remove_subformulas [FormulaOps] 
"Erase" indicated subformulas from the formula.

rename_clauses [GDL] 
Rename clauses so that they have disjoint variables.

rename_quant_avoiding [FormulaOps] 
Rename quantified variables avoiding the ones from
avs ,
and the abovequantified ones.

reorder_clauses [GDL]  
repeating_key_sorted [Aux] 
Checks for a repeating key in a sorted association list.

replace [Term.TermHashtbl]  
replace_assoc [Aux] 
Replace the value of a first occurrence of a key, or place it at
the end of the assoc list.

replace_charprop [Aux] 
Replace characters satisfying
f by repl .

replace_names [Structure] 
Replace the names of elements by new maps.

report_sign_ratio [Rationals]  
reset [SatSolver.S]  
reset_fresh_count [ParseArc] 
Reset the variable suffix count.

restart [SatSolver.S]  
restore_program [GDL]  
result_of_sd [SyntaxDef]  
rev_assoc [Aux] 
Return first key with the given value from the keyvalue pairs,
using structural equality.

rev_assoc_all [Aux] 
Inverse image of an association: return all keys with a given
value (using structural equality).

rev_int_to_string_map [Structure] 
Reverse a map: make an int StringMap from a string IntMap.

rev_string_to_int_map [Structure] 
Reverse a map: make a string IntMap from an int StringMap.

rewrite [Rewriting] 
Rewrite a Term using the set of rules.

rewrite_rule_cons_name [BuiltinLang]  
rewrite_rule_name [BuiltinLang]  
rewrite_rule_tp [BuiltinLang]  
rewrite_single [ContinuousRule] 
For now, we rewrite only single rules.

rewrite_single [DiscreteRule] 
Rewrite the model using the rule at the given matching.

rewrite_single_nocheck [ContinuousRule] 
For now, we rewrite only single rules, but with universal
univs .

rhs [ContinuousRule]  
rk4_step [Formula] 
Perform a RungeKutta (RK4) step for
vars with vals_init and righthand
side eq_terms .

rk4_step_symb [FormulaOps] 
Perform a RungeKutta (RK4) step for
vars with vals_init and righthand
side eq_terms .

rkCK_default_start [Formula] 
Implements the CashKarp algorithm with varying order and adaptive step,
precisely as described in the paper "A Variable Order RungeKutta Method
for Initial Value Problems with Varying RightHand Sides" by J.

rkCK_step [Formula]  
round_futur_last_digit [Integers]  
round_ratio [Rationals]  
rule_obj_str [DiscreteRule] 
Alternative syntax for testing.

rule_str [DiscreteRule]  
rules_for_player [Arena] 
Rules with which a player with given number can move.

rules_of_clause [GDL]  
run_prolog_aggregate [GDL] 
The interpreter can reinterpret "does" atoms as "legal" atoms for
aggregate playout.

run_prolog_atom [GDL] 
Compute all implied instantiations of the given atom, return
sorted unique instances.

run_prolog_check_atom [GDL]  
run_prolog_check_goal [GDL]  
run_prolog_goal [GDL] 
Just check if the atom / conjunction of literals is
satisfiable.

run_shell [TRS] 
A full run of the TRS computation.

run_shell_str [TRS] 
Simplified interface to TRS computation, returns the messages,
resulting system and the list of parsed terms, chronologically.

S  
s_isubst_map_some [Term]  
s_subst_str [Term]  
s_vars_in_term [Term] 
List variables in the given term.

sat [RealQuantElim]  
sat [Sat] 
Check satisfiability of a formula in CNF, return a satisfying assignment.

sat_of_qbf [QBF] 
Reduce QBF to SAT by taking all possibilities for universal variables.

saturate [GDL]  
saturation_engine [TranslateGame] 
Use saturationbased Datalog engine instead of a Prolog interpreter.

sb_str [GDL]  
scharr_x [Picture]  
scharr_y [Picture] 
Gaussian smoothing operator.

separate_disj [TranslateFormula] 
Exposed for testing purposes only.

set_bit [Bitvector] 
Set the bit at the given position to 1.

set_prop_name [BuiltinLang]  
set_timeout [TranslateGame]  
set_timeout [GDL]  
set_timeout [Play]  
set_timeout [Solver.M] 
Set timeout function.

set_timeout [Sat] 
Set timeout function for conversions.

set_timeout [SatSolver.S]  
set_to_set_list [Assignments] 
Create a set_list

set_vals_of_sys [TRS] 
Get set values (chronologically) from a TRS.

shape [Diagram] 
Shape of a weightbased diagram as a canonical int diagram.

short_term [Coding] 
A concise, without supertypes, readable but not parseable form.

short_term [Term]  
sign_big_int [Integers] 
Return
0 if the given big integer is zero,
1 if it is positive, and 1 if it is negative.

sign_int [MiscNum]  
sign_num [Numbers] 
Return
1 , 0 or 1 according to the sign of the argument.

sign_op_str [SignTable] 
Print a sign_op as string.

sign_op_str [Formula] 
Print a sign_op as string.

sign_ratio [Rationals]  
simp_const [Poly] 
Basic simplification, reduces constant polynomials to integers.

simplify [GameSimpl]  
simplify [RealQuantElim]  
simplify [FormulaOps] 
Recursively simplify a formula

simplify [QBF] 
Recursive QBF simplification.

simplify [Sat] 
Given a list of literals to set to true, simplify the given CNF formula.

simplify_formula [QBF] 
Given a formula, simplify its Boolean structure.

simplify_re [FormulaOps] 
Recursively simplify a real expr

simplify_sat [RealQuantElim]  
simult_subst [GDL]  simult_subst ps s t substitutes s at all t paths that belong
to the set ps , returns $tps \ot s $.

singletons [Diagram.S] 
All singletons true in a diagram.

size [GameTree] 
Number of nodes in the tree.

size [Diagram.S] 
The size of a diagram  as a dag (first) and as a tree (second).

size [BoolFunction] 
Compute the size of a Boolean function.

size [QBF] 
Size of a QBF  as a dag and as a tree.

size [Formula]  
size_real [Formula]  
size_up_to [Term] 
Size of a term up to a given value

slist [Assignments] 
List a set or list ref; changes from set to list if required.

sllen [Assignments]  
smallSIZE [Diagram] 
Suitable small size for hash modules.

snd3 [Aux]  
so_compare_weight [Formula] 
Weight of SO atoms when comparing, defaults to 1.

so_to_qbf [Solver] 
Compute the QBF equivalent to the given SO formula on the given structure.

so_var_of_string [Formula]  
sobel_x [Picture] 
Sobel differential operator.

sobel_y [Picture] 
Scharr differential operator.

solve [SignTable] 
Given cases and polynomial array as constructed by
build_cases and
requirement list for some polynomials, return all satisfying cases.

solve [SatSolver.S]  
solve_cnf [SatSolver.S]  
solve_lfp [BoolFunction] 
Inline and solve fixedpoints in the definitions.

solver [SatSolver] 
Set the solver to use.

some [Aux] 
Constructors and unConstructors.

sorted_diff [Aux] 
Set difference of lists of unique increasing elements (as returned
by
Aux.unique_sorted ).

sorted_inter [Aux] 
Set intersection of lists of unique increasing elements (as returned
by
Aux.unique_sorted ).

sorted_merge [Aux] 
Set union of lists of unique increasing elements (as returned
by
Aux.unique_sorted ).

sorted_multiset_union [Aux]  
special_rel_of [DiscreteRule]  
split [Class] 
Split of a sentence on a class definition is either true/false if the class
definition is a Struct s (depending on whether s = phi or not), or a new
sentence psi such that, e.g.

split_charprop [Aux] 
Split a string on characters satisfying
f .

split_chars_after [Aux] 
Look for characters from the list
l after c , split on such pairs.

split_empty_lines [Aux] 
Split a string on empty lines (\n\n).

split_input_string [ParseArc]  
split_newlines [Aux] 
Split a string on newlines (\n or \r).

split_sd_name [SyntaxDef]  
split_sdef_name [Coding]  
split_simplify [Class] 
Split the formula as above and simplify by replacing trivially true
or false atoms such as L(x:R) ...

split_spaces [Aux] 
Split a string on spaces.

split_to_list [Term] 
Lexer for terms and types in internal format, to list

sprint [ContinuousRule]  
sprint [Structure]  
sprint [BoolFunction] 
Another name for sprint.

sprint [Formula]  
sprint_def [BoolFunction] 
Another name for sprint_def.

sprint_defs [BoolFunction] 
Another name for sprint_defs.

sprint_full_length_int [MiscNum]  
sprint_game_move [Arena]  
sprint_ppm [Picture] 
Print a picture in the simple PPM format to a string.

sprint_real [Formula]  
sprint_rule [DiscreteRule]  
sprint_state [Arena] 
Print the structure in extensive form.

sprint_state_ext [Arena] 
For the rules of the game, also print their compiled forms.

sprint_state_full [Arena]  
sset [Assignments]  
state [GameTree] 
State in the given node.

state_cls [GDL]  
state_str [Arena] 
Print the whole state: the game, structure, time and aux data.

state_terms [GDL]  
static_rels [GDL] 
Partition relations into static (not depending, even indirectly,
on "true") and remaining ones.

step_shell [TRS] 
A full one step of the computation.

str [Reduction] 
Print a reduction

str [GameTree] 
Game tree printing function.

str [Arena]  
str [ContinuousRule] 
Print a rule to string.

str [Class] 
Print a regular structure class as a string, using its definition.

str [Poly] 
Print a polynomial as a string.

str [OrderedPolySet] 
Print the given set as string.

str [OrderedPoly]  
str [Assignments] 
Print the given assignment as string.

str [Structure] 
Print the structure
struc as string.

str [Bitvector] 
Print the bit vector to string.

str [Diagram.Variables]  
str [BoolFunction] 
Print to formatter.

str [Formula] 
Print a formula as a string.

str_abstract [GameTree] 
Abstract tree printing function.

str_contains [Aux] 
Checks whether the first argument contains the second one.

str_def [BoolFunction] 
Print definition to formatter.

str_defs [BoolFunction] 
Print definitions to formatter.

str_index [Aux] 
Index of the first occurence of the first argument in the second one.

str_subst_all [Aux] 
Substitute all ocurrences of the first argument by the second one.

str_subst_all_from_to [Aux] 
Substitute all ocurrences of the interval between
the first argument and the second one by the third one.

str_subst_once [Aux] 
Substitute the first ocurrence of the first argument by the second one.

str_subst_once_from_to [Aux] 
Substitute the first ocurrence of the interval between
the first argument and the second one by the third one.

string_cons_name [BuiltinLang]  
string_name [BuiltinLang]  
string_of_big_int [Integers] 
Return the string representation of the given big integer,
in decimal (base 10).

string_of_num [Numbers]  
string_of_ratio [Rationals]  
string_of_value [SatSolver]  
string_quote_name [BuiltinLang]  
string_quote_rules [Coding]  
string_tp [BuiltinLang]  
strings_of_list [Aux]  
strip_charprop [Aux] 
Strip characters satisfying
f from left and right of a string.

strip_spaces [Aux] 
Strip spaces from left and right of a string.

strmap_filter [Aux]  
strmap_of_assoc [Aux]  
struc_from_trs [Structure] 
Parse the TRS string, output messages and the resulting structure.

struct_sum_str [Class] 
Print a class definition (right hand side) as string.

sub [OrderedPoly]  
sub_big_int [Integers] 
Subtraction.

sub_ratio [Rationals]  
subst [GDL]  
subst [QBF] 
Substitute for variables in a QBF.

subst_clause [GDL]  
subst_consts [GDL]  
subst_consts_clause [GDL]  
subst_consts_literals [GDL]  
subst_literal [GDL]  
subst_literals [GDL]  
subst_mod_vars [BoolFunction] 
Substitute module variables.

subst_name_avoiding [FormulaSubst] 
Find a substitution for
v which avoids avs .

subst_name_avoiding_str [FormulaSubst] 
Find a substitution for
v which avoids avs , string arguments.

subst_name_prefix [FormulaSubst] 
Prefix for variable name replacements.

subst_once_rels [FormulaSubst] 
Substitute once relations in
defs by corresponding subformulas
(with instantiated parameters).

subst_once_rels_expr [FormulaSubst]  
subst_real [FormulaSubst] 
Substitute a real variable with a subexpression.

subst_rel [GDL]  
subst_rels [GDL]  
subst_rels [FormulaSubst] 
Substitute recursively relations defined in
defs by their definitions.

subst_rels_expr [FormulaSubst]  
subst_t_pos [Term]  
subst_vars [FormulaSubst] 
Apply substitution
subst to all free variables in the given formula
checking for and preventing name clashes with quantified variables.

subst_vars_expr [FormulaSubst]  
substs_fstr [Term]  
substs_str [Term]  
suffix [Term] 
Suffix all type variables, useful for renaming.

suggest_expansion [Heuristic] 
Whether a formula should be considered for expansion: has a
universal quantifier or the number of its existential quantifiers
is smaller than
suggest_expansion_coef times the
square root of the number of elements in the structure.

sum [Assignments] 
Sum of two assignments, assuming that
elems are all assignable elements.

sum_gt0 [QBF] 
QBF saying if the sum of signed numbers (lowerendian) is > 0.

super_canny [Picture]  
symbol_of_term [Term] 
Head symbol, i.e.

syntax_definition_decl_name [BuiltinLang]  
syntax_definition_name [BuiltinLang]  
syntax_definition_tp [BuiltinLang]  
syntax_definition_type_var_b_name [BuiltinLang]  
syntax_definition_type_var_name [BuiltinLang]  
syntax_definition_var_name [BuiltinLang]  
syntax_definition_var_op_name [BuiltinLang]  
syntax_defs_of_sys [TRS] 
Get syntax definitions from a TRS.

syntax_element_list_cons_name [BuiltinLang]  
syntax_element_list_elem_name [BuiltinLang]  
syntax_element_list_name [BuiltinLang]  
syntax_element_list_tp [BuiltinLang]  
syntax_element_name [BuiltinLang]  
syntax_element_str_name [BuiltinLang]  
syntax_element_tp [BuiltinLang]  
syntax_element_tpcons_name [BuiltinLang]  
syntax_elems_of_sd [SyntaxDef]  
syntax_ok [Formula] 
We check that relations and SO variables appear with unique
arities and that fixedpoint variables appear only positively.

syntax_ok_re [Formula]  
sys_big_int_of_string [Integers]  
T  
t_isubst_map [Term]  
t_isubst_str [Term]  
t_subst_str [Term]  
t_vars_in_term [Term]  
take_n [Aux] 
Take
n elements of the given list, or less it the list does not
contain enough values.

take_n_with_rest [Aux] 
Take
n elements of the given list, or less it the list does not
contain enough values.

tc [LearnGame] 
A flag whether to use the TC operator or not.

tc_atomic [Distinguish] 
Pairs (n, phi) such that phi is a twovariable
?positive atomic formula
and the nstep transitive closure of phi holds somewhere on struc .

tc_atomic_distinguish [Distinguish] 
Find a upto
n step transitive closures of twovariable ?positive atomic
formulas that hold on all pos_strucs and on no neg_strucs .

tc_max [Distinguish] 
Maximum n between
from and upto such that nstep TC of phi holds.

term_arities [GDL]  
term_of_sd [SyntaxDef] 
A helper function returning type with level indication, or ?t.

term_of_string [Coding]  
term_paths [GDL] 
All paths in a term pointing to subterms that satisfy a
predicate.

term_str [GDL]  
term_str [Term] 
Concise readable form.

term_term_cons_name [BuiltinLang]  
term_to_name [GDL]  
term_to_string [Coding]  
term_tp [BuiltinLang]  
term_tp_name [BuiltinLang]  
term_type_var_b_name [BuiltinLang]  
term_type_var_name [BuiltinLang]  
term_var_cons_name [BuiltinLang]  
term_vars [GDL]  
terms_of_list [GDL]  
terms_str [GDL]  
terms_vars [GDL]  
ternary_truth_value_tp [BuiltinLang]  
ternary_unknown_name [BuiltinLang]  
tnf [FormulaOps] 
Convert formula to TNF; or negTNF when
neg is set.

tnf_fv [FormulaOps] 
first existentially quantifies free vars

tnf_re [FormulaOps]  
to_array [QBF] 
Helper function  put a list into an array of length k,
pad with false, return whatever is left over.

to_cnf [FormulaOps] 
Convert an arbitrary boolean combination to CNF.

to_const [Formula] 
Casts to particular variable types.

to_const_or_fo [Formula]  
to_dnf [FormulaOps] 
Convert an arbitrary boolean combination to DNF.

to_fo [Formula]  
to_int [Diagram.Variables]  
to_list [Bitvector] 
The list of set bits.

to_real [Formula]  
to_rev_list [Bitvector] 
The list of set bits, in reverse order.

to_so [Formula]  
top_reduce [Diagram.S] 
Reduction from top.

top_sat [Diagram.S] 
Sat check by reduction from top.

topol_sort [Aux] 
Topogical sort of
l where cmp a b = true means that there is
an arrow from a to b .

topsort_callgraph [GDL]  
translate [TranslateFormula] 
Translate a disjunction of conjunctions of literals (and disjs of
lits).

translate_from_precond [DiscreteRule] 
Build a rule by translating the "add" list into the RHS structure
directly, and separating out from a precondition the LHS structure
over the
struc_vars variables.

translate_game [TranslateGame]  
translate_incoming_move [TranslateGame]  
translate_outgoing_move [TranslateGame]  
transpose [Matrix]  
transpose_lists [Aux] 
Transpose a rectangular matrix represented by lists.

trd3 [Aux]  
triv_simp [BoolFunction] 
Flatten and perform trivial simplifications (e.g.

triv_simp_defs [BoolFunction] 
Trivial simplification of Boolean definitions.

trs_set_struc [Structure] 
Apply TRS values to a structure.

tuples [Assignments] 
List all tuples the firstorder assignment
asg assigns to vars
in order in which vars are given.

tuples_of_list [Structure]  
type_with_level_of_sd [SyntaxDef]  
types_of [Term]  
U  
unary_add [QBF]  
unfold [GameTree] 
Game tree unfolding.

unfold_abstract [GameTree] 
Abstract game tree unfolding function, calls argument functions for work.

unfold_maximax [Play] 
Maximax by depth unfolding function.

unfold_maximax_upto [Play] 
Maximax unfolding upto iterations, keep previous moves for stability.

unhc [Formula] 
Unhashcons a formula.

unhc_real [Formula] 
Unhashcons a real expression.

unify [GDL]  
unify_all [GDL]  
unify_args [GDL] 
Match terms on the left to ground terms on the right, ignoring
Const "_BLANK_" on the right.

unify_rels [GDL]  
union [OrderedPolySet]  
unique [QBF] 
Helper function: list of unique qbfs from l, in unspecified order.

unique [Aux] 
Return the list of unique elements, under the given comparison
(the input does not need to be sorted).

unique_append [Aux]  unique_append l1 l2 appends elements not occurring in l2 to
it, without repeating elements.

unique_name_of_sd [SyntaxDef]  
unique_sorted [Aux] 
Return the list of structurally unique elements, in order sorted
by
Pervasives.compare .

unit_big_int [Integers] 
The big integer
1 .

universal [Assignments] 
Project assignments on a given universal variable.

universal_list [Assignments]  
universal_tvar_b_name [BuiltinLang]  
universal_tvar_name [BuiltinLang]  
unpack_te [Coding] 
Remove parse level information from the head of the term.

unsafe_add_rel [Structure] 
Add tuple
tp to relation rn in structure struc without
checking whether it and its elements already exist in the structure
and without checking arity.

unsafe_add_rels [Structure] 
Add tuples
tps to relation rn in structure struc without
checking for elements existence and arity matching.

unsigned_gt [QBF] 
QBF saying if one number (unsigned lowerendian) is greater that another.

unsome [Aux]  
update_assoc [Aux] 
Update the value associated with the first occurrence of the key,
if no key is present update the given default "zero"
value.

update_on_term [TRS]  
use_monotonic [Heuristic]  
use_sum_gates [QBF] 
Whether to use DNF or TC=sums as gates in convolution.

V  
value_i_name [BuiltinLang]  
value_level_name [BuiltinLang]  
value_of [SatSolver.S]  
value_pref [BuiltinLang]  
var [OrderedPoly]  
var_list_str [Formula] 
Print a variable list as a string.

var_of_string [Formula] 
We recognize if the variable is FO (x), MSO (X), SO (x) or Real (:x).

var_of_term [TranslateFormula]  
var_str [Formula] 
Print a variable as a string.

var_subst [FormulaSubst] 
Helper function: apply subsutitution
subst to the variable v .

var_tup [Formula]  
vars [Poly] 
List variables in the given polynomial.

vars [Diagram.S] 
All variables in a diagram, with the number of path they appear on.

vars_list [Poly] 
List variables in the given polynomial list.

verbatim_name [BuiltinLang]  
verbatim_rules [Coding]  
W  
weights_array [Diagram] 
Simply set this array to the weights of integers in your diagrams.

win_so_formula [Arena]  
Z  
zero_big_int [Integers] 
The big integer
0 .

zeroes [Matrix.MAT] 