Index of values

( * ) [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]

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 counter-example 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]
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 well-formed, check if it will remain well-formed 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 nth 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 non-fixed-point 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]
Fold-left on two arrays.
array_fold_map2 [Aux]
Fold-left 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 position-dependent 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 index-wise.
array_map_of_list [Aux]
Same as Array.of_list ( 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 ith 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 MSO-variable.
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]

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 (2-complement) 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]
Color-encode 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]
Floating-point 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]

cAnd [Diagram.S]
cAnd [Formula]
Hash-cons 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.
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 first-order 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 hash-consing 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 bit-images of size XxY.
copy [Term.TermHashtbl]
counter_n [GDL]
create [Term.TermHashtbl]
create [HashCons.S]
Create a new hash-consing 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]

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 top-most 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 n-dimensional formula for structures of given size.
dimension_vars [FormulaOps]
Make the list of FO variable names n-dimensional.
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.

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 non-wildcard 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_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 variable-sharing "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 counter-exaples.
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 counter-examples.
find_reduct_iter_counterexample [Reduction]
Return the current counterexample structure.
find_reduct_iter_start [Reduction]
Find reduction iterating on counter-exaples as above - start
find_reduct_iter_step [Reduction]
Find reduction iterating on counter-exaples as above - step
find_rel_arg [GDL]
find_so [Solver]
Find assignment for second-order 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 floating-point 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 center-of-gravity 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 un-applied 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.

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 pre-processed 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.

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]
Hash-cons a formula.
hc_real [Formula]
Hash-cons a real expression.
head_grounding [Term]
Identity on non-variable 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]

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 non-fixed-point definitions.
input_rewrite_rule_name [BuiltinLang]
input_rewrite_rule_tp [BuiltinLang]
insert [Aux.PRIOQUEUE]
insert_nth [Aux]
Insert as nth 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 ISA-matching or raises UNIFY.
isa_unify [Term]
Returns the ISA-unification: like ISA-matching, 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.

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".

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 two-player win-lose-or-tie 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]
Tail-recursive 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 (base-3) 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.

make_empty [Aux.PRIOQUEUE]
make_fo_tc_conj [FormulaSubst]
First-order k-step refl.
make_fo_tc_disj [FormulaSubst]
make_fold [FormulaMap]
make_fp_inductive [FormulaOps]
Replace fixed-points 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_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 key-value 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_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 top-level formulas in the real expression (Chars 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]
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 less-or-equal comparison.
maximal_o [Aux]
Return single maximal element (in case of "less" or "less-or-equal" comparison) .
maximal_unique [Aux]
Return the list of all maximal elements, under the given less-or-equal comparison.
maximax_unfold_choose [Play]
Maximax unfold upto iterations and choose move.
maxpool [QBF]
Max-pool a XxY bit-image to a (X/2)x(Y/2) bit-image.
mem [Term.TermHashtbl]
mem_rev_assoc [Aux]
Check if the value is associated with a key in the key-value 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]

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

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_pn_nnf [FFTNF]
Prenex-normal 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 piecewise-linear 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 [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 reduction-finding 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]
Fixed-point 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]

qbf_hc [QBF]
Hash-cons 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.

random_elem [Aux]
Random element of a list.
range [FormulaSubst]
Rough estimate of the range of a real-valued expression given structure size and function, real-variable value and predicate size estimates.
range [Aux]
Returns an int list from from (default 0) to k-1.
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 bit-matrices.
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 edge-separated regions, region numbers start from 1, remaining edges are pseudo-region 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 above-quantified 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 key-value 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 Runge-Kutta (RK4) step for vars with vals_init and right-hand side eq_terms.
rk4_step_symb [FormulaOps]
Perform a Runge-Kutta (RK4) step for vars with vals_init and right-hand side eq_terms.
rkCK_default_start [Formula]
Implements the Cash-Karp algorithm with varying order and adaptive step, precisely as described in the paper "A Variable Order Runge-Kutta Method for Initial Value Problems with Varying Right-Hand 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_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 saturation-based 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 weight-based 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 fixed-points 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]
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 (lower-endian) 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 fixed-point variables appear only positively.
syntax_ok_re [Formula]
sys_big_int_of_string [Integers]

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 two-variable ?positive atomic formula and the n-step transitive closure of phi holds somewhere on struc.
tc_atomic_distinguish [Distinguish]
Find a upto-n-step transitive closures of two-variable ?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 n-step 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 first-order 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]

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]
Un-hash-cons a formula.
unhc_real [Formula]
Un-hash-cons 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
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 lower-endian) 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.

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]

weights_array [Diagram]
Simply set this array to the weights of integers in your diagrams.
win_so_formula [Arena]

zero_big_int [Integers]
The big integer 0.
zeroes [Matrix.MAT]