Index of values

Bitwise and.

Function composition.

Bitwise or.

Absolute value.

Absolute value.

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

Addition.

Add a new constant.

Add defined functions to a structure.

Add defined relations to a structure.

Add element e to struc if it is not yet there.

Add a rewriting rule: whether the rewritten term has to be ground, LHS and RHS -- to the set, at the start.

Add function assignment e -> x to function fn in structure struc.

Add function assignments assgns to fn in structure struc.

Addition of a small integer to a big integer.

Add a rewriting rule to the set, at the end.

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

Assign models to elements by f in struc, replacing previous.

Add new element to struc, return the updated structure and the element.

Add tuple tp to relation rn in structure struc.

Ensure relation named rn exists in struc, add if needed.

Add tuple tp to relation rn in structure struc.

Add tuples tps to relation rn in structure struc.

Assuming that the given set of declarations is well-formed, check if it will remain well-formed after adding the given declaration.

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

An nth cartesian power of the list.

All subsets of a given set of size up to max_size.

All variables in a formula.

Insert non-fixed-point definitions into a function.

Apply f to left (if to_left) or right side of the given rule.

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

Zip two arrays into an array of pairs.

Find all elements for which f holds.

Find indices of all maximal elements in an array.

Fold-left on two arrays.

Fold-left and map on two arrays.

As Array.fold_left, but with the element position passed.

Find if a predicate holds for all elements.

For all on two arrays.

Find if a position-dependent predicate holds for all elements.

Make an array from an association from indices to values.

Iterate an action over all elements of two arrays pointwise.

Map a function over two arrays index-wise.

Same as Array.of_list (List.map f l)

Map an array filtering out some elements.

Return a copy of array with the ith element replaced by elem.

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

Assign emptyset to an MSO-variable.

Elements assigned to a given FO variable.

Variables assigned in an assignement set.

Create an assignment set out of an array of variables and a list of assigned tuples.

Return all values of a key.

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

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.

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

The list of literals which hold for a tuple on a structure, i.e.

All atoms over given signature and variables.

AType with variables over given relations, no repetition, equality.

Basic outline of the form "ex x_1 ..

Print a Boolean formula as a string.

Suitable big size for hash modules.

Convert a small integer to a big integer.

Convert a natural to a big integer.

Convert a string to a big integer, in decimal.

Given a signed binary number n returns |n|.

Binary addition.

Given (binary) number n returns -n in our (2-complement) representation.

Binary subtraction.

Color-encode numbers, 0 remains black, possible clashes.

Board element name under given coordinates, column first.

Coordinates, column first, of a board element name.

Floating-point matrix of brightness in range 0..1.

Import from unordered generic type.

Build array of polynomials and cases to check given set of polynomials.

Hash-cons a conjunction.

Smart constructors, cAnd hashes and enforces the assertions (0) - (4).

Default number of sample points per parameter in tree search.

How to exchange payoffs for heuristics.

This function allows to add cached expanded forms; for speed only!

Detect edges: hi_thr how insensitive to new edges, lo_thr how insensitive to edge continuations, extend how many pixels to prolong existing edge.

Change function fn assignment for element e to x in struc.

Relations that can explicitly change state by rewriting (i.e.

Check the formula on the structure.

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 if a relation holds for a tuple.

Check if given float has sign as required by the sign_op.

Check whether the term belongs to the given class.

Select an arbitrary assignment for first-order variables with the given names and default values.

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

Choose all maximizing moves given a game tree.

Return the given clause (disjunction of literals) as string.

Changes a string s to use only alphanumeric characters and underscore and to start with a lowercase letter.

Clears the hash table.

Clear the given hash-consing table.

Clear the bit at the given position, i.e.

Clear cache.

Remove the given function from struc.

Remove element names from structure.

Clear QBF consing table -- only for strict test repeatability.

Remove all relations matching the predicate.

Clear timeout function.

Clear timeout function.

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

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.

Compare by weight if present in array, else simply the natural order.

Return the given CNF formula as string.

Collects elements by key (returns a list sorted by key).

Equality check on structures.

Compare two formulas.

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 two (game, state) pairs and explain the first difference met.

Compare two rules and explain the first difference met.

Compare two rules and explain the first difference met.

Compare two structures and explain the first difference met.

Comparison function for elements.

Compare two real expressions.

Order on types that we use to select the minimal ones.

The order on variables we use; might differ from Formula.compare_vars!

Compare two variables.

Compile eq_sys to function.

Translate a rule specification into a processed form.

Complement an assignment set assuming elems are all assignable elements.

Complement a and join with aset; assumes a is joined with aset

Check whether each of argpaths covers some tree in c_paths completely.

Compress the given assignment set, use number of elements.

Helper function to do the full computation.

concat_foldl f (a::l) init = concat_foldl f l (concat_map (f a) init)

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

Concatenate results of a function.

Return the given conjunction of literals as string.

cons e l = e::l.

Constructur 'Const' but taking normal integers.

Return the assignment of constants in the structure.

Convert a QBF to CNF.

Convert a DNF formula to CNF (or equivalently, CNF to DNF).

Convert a auxiliary CNF formula to "real" CNF (or, equivalently, to DNF).

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

Convolve a NxNxL+1 list of (signed) weights with a list of L bit-images of size XxY.

Create a new hash-consing table of the given size.

Print a QBF formula as a dag.

Compute a decomposition of a formula on a given class definition.

Return the default structure for the circle shape.

Remove the element e and all incident relation tuples from struc.

Remove elements es and all incident relation tuples from struc.

Remove the tuple tp from relation rn in structure struc.

Remove the tuples tps from relation rn in structure struc.

Delete top-most quantification of vs in the formula.

If false, dimacs files generated for external solvers will be preserved.

Create a diagram from a CNF.

Make a diagram of a QBF.

Print a diagram as a formula.

Elements from s1 which differ in s2, with differing relation names.

Differentiate all polynomials in the given set.

Differing relations (used in solver cache)

Create a n-dimensional formula for structures of given size.

Make the list of FO variable names n-dimensional.

Convert a term to string concisely using the Greatest Lower Bound notation.

Find a formula holding on all pos_strucs and on no neg_strucs.

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.

Number of steps and base formula if distinguish returns a TC.

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

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

Euclidean quotient of two big integers.

Convert a function to DNF with eliminated quantifiers.

Return the given DNF formula as string.

The element name of an element (given by integers)

The integer corresponding to a given element name.

Print a parser elem.

Print the elements e as string.

Return the list of elements in a structure.

Return the set of elements in a structure.

Return the elements on which function f has value x in struc.

Top variable elimination until size, else branch elimination.

Sat check based on elim_bounded.

Eliminate arguments of relations that are defined by non-wildcard pattern matching (i.e.

Sat check by repeated top variable elimination.

Eliminate the top variable recursively up to the given size.

Eliminate an existential variable (or universal, if set).

Empty bit vector.

Empty rule.

Operations on substitutions.

Find a term corresponding to the name of a variable or raise Not_found.

Return the empty structure (with empty signature).

Return the empty structure with given relational signature.

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

Add path to a set.

Check for equality but ignore RHS subterms corresponding to LHS type variables.

Enforce that in aset the variable u is equal to w.

Whether to print relation definitions as equations, or using the C syntax.

Counter of internal formula evaluations for profiling.

Evaluate the formula on the structure.

Evaluate the formula on the structure and join with given assignment.

Evaluate real expressions.

Expand branches of a definition inlining the provided definitions.

Expand Let's and RLet's in formula.

Returns a disjunction of existentially quantified conjunctions of atoms each disjunct being equivalent to the given formula in the given model.

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

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

Extends all the arcs in the given list that can be extended and removes all other arcs.

Return the list of functions.

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.

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 an example structure of a given size for a formula.

Find the index of the first occurrence of a value in a list, counting from zero.

Find lfp formula iterating on counter-exaples.

Find all embeddings of a rule.

Find a model for a QBF formula.

Find a model for a quantifier free QBF formula.

Find an element in the structure, and if not present, add new one.

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

Find reduction iterating on counter-examples.

Return the current counterexample structure.

Find reduction iterating on counter-exaples as above - start

Find reduction iterating on counter-exaples as above - step

Find assignment for second-order variables and add it to the structure.

Find the first element of the list on which the function does not raise Not_found and return its result.

Flatten conjunctions and disjunctions.

Only flatten the formula.

Helper function to flatten multiple or's, and's, and quantifiers.

Flatten and sort multiple or's and and's.

Flip a picture.

Returns a floating-point number approximating the given big integer.

A fluent precondition is an approximation to the condition on a structure for the positive/negative fluent to appear/disappear at a position.

Fluents are relations that are changed by rules.

Convert an association list into an assignment for FO variables.

Convert the FO part of an assingment set into a list of substitutions.

Parameter governing whether to use LFP or FO TC when parsing.

Fold the structure using the operations.

Fold f over the list collecting results whose computation does not raise Not_found.

Iterate a function n times: f^n(x).

Irrespective of the shape of payoffs, take the difference of heuristics as the final heuristic for each player (in Heuristic.default_heuristic_old).

Variable ordering heuristiv called FORCE, a center-of-gravity positioning based simulation of MINCE, from the paper by Aloul, Markov and Sakallah.

Convert an arbitrary formula to CNF via Boolean combinations.

Print an equation system.

Print a picture in the simple PPM format to a formatter.

Print the relation with tuples ts.

Print an unboxed separated list, with breaks after the separator.

Return a structure with a single relation of given arity, over a single tuple, of different elements.

Free variables in a QBF.

Free variables in a formula.

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

The name for function type (type of un-applied function term).

Return the value of function f on e in struc.

Functions in the structure.

Remove the elements that are not incident to any relation (and have no defined properties, unless ignore_funs is given).

Greatest common divisor of two big integers.

Saturation currently exposed for testing purposes.

Export to unordered generic type.

All atoms in a formula.

Get the bit at the given position.

Get a managed (data, data) cache.

Get a managed (data, 'a) cache.

Get a managed (data * data, data) cache.

Get a managed (data * data, other_value) cache.

Get the value of a real expression without free variables.

All relations in a formula, with arities, and constants that appear.

Greatest Lower Bound Unification w.r.t.

Builtin syntax definitions to introduce when building a TRS.

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.

Usual boolean comparisons between two big integers.

Print a guard tuple, as returned above, to string.

Guarded ?existential qr-type in length of tuple-variables of tuple in struc.

All guarded ?existential types of rank qr of guarded k-tuples in struc.

Generate all guarded substitutions of tuple with the guards.

Check if a qbf has quantifiers inside.

Hash size used when making the module.

A hashing function for 'a hc lists.

Hashcons a value.

Hash-cons a formula.

Hash-cons a real expression.

Identity on non-variable terms, return type of sharing variable and upper bound of type variable.

Identity map to be refined using the with syntax.

Fill the RGB channels from floats in range 0..1.

Return the list of relation tuples incident to an element e in struc.

Maps from an array to another array of possibly different type.

Game tree initialization.

Abstract initialization function.

Inline all non-fixed-point definitions.

Insert as nth element of a list (counting from zero).

Print a case, i.e.

Convert a big integer to a small integer (type int).

Remove level prefixes and indicators from the head of the term.

The inverse map of element names.

Check variable type.

Check if a bitvector is empty.

Test whether the given big integer is small enough to be representable as a small integer (type int) without loss of precision.

Is the number an integer?

Check satisfiability of a formula in CNF, return just true or false.

A very quick check that ignores all subterms, if a term is a superclass of another term (or the same class).

Character classes.

Returns the ISA-matching or raises UNIFY.

Returns the ISA-unification: like ISA-matching, but does not treat the RHS type variables as constants, instead infers their upper bounds.

Iterate given function on all variables of the qbf.

This function joins two assignment sets, i.e.

Given two sign_ops x and y return a sign op for "x and y".

Print a label as a string.

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.

Extract leading coefficients from all polynomials in the set.

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.

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.

Set difference: List.filter (fun e -> not (List.mem e b)) a.

Find all maximal elements in a list.

Printf helper functions.

Create a list of given length initialized from the indices.

Intersection: list_inter a b = List.filter (fun e -> List.mem e b) a.

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

As list_moves but with animation shifts for each move.

Remove all elements equal to the argument, using structural equality.

Tail-recursive List.split with accumulators; reverses the lists.

Log a variable, diagram and variable assignment.

Estimate the (base-3) logarithm of the number of cases needed for pset.

Least Upper Bound Unification w.r.t.

First-order k-step refl.

Replace fixed-points by their inductive evaluation for given size.

Make a layer of a convolutional network with k maps.

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

Make a move in a game.

Transitive closure of phi(x, y, z) over x and y, an MSO formula.

Make an ordered polynomial from p with prio_list order on variables,i.e.

Make ordered polynomials from ps with prio_list order on variables.

Make ordered polynomials from first components of ps, prio_list order.

Create a continuous rule given a named discrete rule and other params.

The default TC syntax: LFP if fo_tc_param = 0 else FO with fo_tc_param.

Maps a function to all polynomials in the set.

Rewrite numeric constants inside an expression.

Map through the structure adjusting subformulas/subexpressions.

Map optional value, with a default result for the None case.

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 a second list and prepend the result to the first list, by single traversal.

Map elements into key-value pairs, and fold values with the same key.

Map a list filtering out some elements.

Map

Map f to all atoms in the given formula.

Map to the structure representation of discrete part of rules.

Map and fold over formulas in a rule.

Map f to top-level formulas in the real expression (Chars and Sum guards).

Map f to all literals (i.e.

Map f on the list collecting results whose computation does not raise Not_found.

Check for equality modulo ground terms on the right.

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

Application of term substitutions (only flat functional substitutes).

Matches which satisfy postcondition with time 1 and empty params

Translate from names to elements to get rule embedding.

Printing.

Return the greater of its two arguments.

Maximal variable number occuring (positively or negatively) in phi.

Return the list of all maximal elements, under the given less-or-equal comparison.

Return single maximal element (in case of "less" or "less-or-equal" comparison) .

Return the list of all maximal elements, under the given less-or-equal comparison.

Maximax unfold upto iterations and choose move.

Max-pool a XxY bit-image to a (X/2)x(Y/2) bit-image.

Check if the value is associated with a key in the key-value pairs, using structural equality.

Merging of two lists, sorts arguments and produces a cmp-sorted list.

The set of paths that merges two terms, the cardinality of this set, and the size of the largest common subtree.

Iterated Substitution based variant of the Most General Unifier substitution, throws UNIFY if not unifiable.

Return the smaller of its two arguments.

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

Greedy minimize the number of between-sep positive variables in a model.

Minimal type satisfying f over rels extending vars.

Unary negation.

Various constructed heuristics.

Conjunction of two diagrams.

Disjunction of two diagrams.

Euclidean modulus of two big integers.

Euclidean division: remainder.

Return the model assigned by f to e in struc.

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.

Print a game as a string.

Multiplication of two big integers.

Multiplication of a big integer by a small integer

Print the given assignment as string, using element names.

The map containing element names.

How many bits to use in numbers or conjunctions in gates.

Number of elements in a structure.

Number of bits set in a vector.

neg f x = not (f x)

Negate a sign_op.

Form clause bodies whose disjunction is equivalent to the negation of disjunction of given clause bodies.

A new set of rewriting rules, containing the given list

Convert formula to NNF and additionally negate if neg is set.

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

Upto this clause number we don't use external solvers (default: 4).

Whether to add root predicates.

Get the stored information of a game tree node.

The values of a game tree node.

Normalise the Term.

Just normalise the special bracketing function.

Normalize

Replace all white space sequences by a simple space, strip on both ends.

Returns a string prolonging s and not appearing in names.

Returns n strings proloning s and not appearing in names.

Check whether the list contains duplicates, using structural equality.

The ?existential qr-type in length of tuple-variables of tuple in struc.

All ?existential types of rank qr of all k-tuples in struc.

Return the number of machine words used to store the given big integer.

Mark the bits at positions given in the list.

Heuristic of payoff expression.

Omit leading coefficients from all polynomials in the given set.

Prenex-normal negation normal form of a formula with minimized alternation and preference to start from existential quantification.

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

We can parallelize computation to a second running Toss client.

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 a reduction.

Partition a list of tagged elements into the Left and Right-tagged elements.

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

List the paths in a set.

Generate a piecewise-linear function of a given argument from a graph.

Player in the given node.

Limit on plys for both aggregate and random playouts.

Besides the aggregate or random playout, also return the separation of rules into static and dynamic.

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

Prenex normal form.

Find the value associated with the first occurrence of the key and remove them from the list.

As Aux.pop_assoc, but uses physical equality.

Find an element satisfying the predicate and separate it from the list.

Power function used in parser.

power dom img generates all functions with domain dom and image img, as graphs.

Some Toss predicates are generated from a path and an expected subterm at that path.

If set, predicates paritition the universe (are disjoint and total).

Print.

Print a QBF formula in cqbf format.

Print definition.

Print definitions.

Print dimacs for a cnf.

Simple heuristic print helper.

Print a 2QBF formula in lparse format.

Print a QBF formula in qdimacs format.

Print a QBF formula in qiscas format.

Print a QBF formula in qpro format.

Print reduction-finding condition in qpro (fmt=0), lp (fmt=1),or qdimacs.

Create a game state, possibly by extending an old state, from a list of definitions (usually corresponding to a ".toss" file.)

Cartesian product of lists.

Size of the cartesian product of lists; max_int if the size is bigger.

Project assignments on a given variable.

Projection on a list of variables.

Promote relations from the given set.

Fixed-point of propagate_once.

Propagate variables and all other singletons.

Remove quantifiers that bind only variables not occurring freely in the body.

Basic pushing of quantifiers inside a formula

Hash-cons a raw QBF formula.

Convert a boolean formula to QBF.

Print a QBF formula.

Quantified variables in a formula.

Euclidean division: quotient.

Euclidean division of two big integers.

Random element of a list.

Rough estimate of the range of a real-valued expression given structure size and function, real-variable value and predicate size estimates.

Returns an int list from from (default 0) to k-1.

Read a picture from a scanning buffer.

Read a PPM grayscale image into a list of 8 bit-matrices.

Read a qdimacs description of a QBF from a string.

Print a real_expr as a string.

If some path points only to bigger than one (i.e.

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.

Average colors per region.

Compute edge-separated regions, region numbers start from 1, remaining edges are pseudo-region 0.

Parameter for dnf conversion in registration.

Graph of a relation in a model, returns an empty set if the relation is not in the signature.

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

Toss relations hold between subterms of GDL state terms: generate Toss relation name.

Return the list of relations with their arities.

Size of a relation, i.e.

Cardinality of graphs of all relations in the structure.

Print the relation named rel_name with tuples ts as string.

Relations in the structure.

Find all positively and negatively occurring relations.

Remove all occurences of the given variable, whatever they mean.

Remove the last element in a list; raise Not_found for [].

Remove an occurrence of a value (uses structural equality).

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.

"Erase" indicated subformulas from the formula.

Rename clauses so that they have disjoint variables.

Rename quantified variables avoiding the ones from avs, and the above-quantified ones.

Checks for a repeating key in a sorted association list.

Replace the value of a first occurrence of a key, or place it at the end of the assoc list.

Replace characters satisfying f by repl.

Replace the names of elements by new maps.

Reset the variable suffix count.

Return first key with the given value from the key-value pairs, using structural equality.

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

Reverse a map: make an int StringMap from a string IntMap.

Reverse a map: make a string IntMap from an int StringMap.

Rewrite a Term using the set of rules.

For now, we rewrite only single rules.

Rewrite the model using the rule at the given matching.

For now, we rewrite only single rules, but with universal univs.

Perform a Runge-Kutta (RK4) step for vars with vals_init and right-hand side eq_terms.

Perform a Runge-Kutta (RK4) step for vars with vals_init and right-hand side eq_terms.

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.

Alternative syntax for testing.

Rules with which a player with given number can move.

The interpreter can reinterpret "does" atoms as "legal" atoms for aggregate playout.

Compute all implied instantiations of the given atom, return sorted unique instances.

Just check if the atom / conjunction of literals is satisfiable.

A full run of the TRS computation.

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

List variables in the given term.

Check satisfiability of a formula in CNF, return a satisfying assignment.

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

Use saturation-based Datalog engine instead of a Prolog interpreter.

Gaussian smoothing operator.

Exposed for testing purposes only.

Set the bit at the given position to 1.

Set timeout function.

Set timeout function for conversions.

Create a set_list

Get set values (chronologically) from a TRS.

Shape of a weight-based diagram as a canonical int diagram.

A concise, without supertypes, readable but not parseable form.

Return 0 if the given big integer is zero, 1 if it is positive, and -1 if it is negative.

Return -1, 0 or 1 according to the sign of the argument.

Print a sign_op as string.

Print a sign_op as string.

Basic simplification, reduces constant polynomials to integers.

Recursively simplify a formula

Recursive QBF simplification.

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

Given a formula, simplify its Boolean structure.

Recursively simplify a real expr

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

All singletons true in a diagram.

Number of nodes in the tree.

The size of a diagram - as a dag (first) and as a tree (second).

Compute the size of a Boolean function.

Size of a QBF - as a dag and as a tree.

Size of a term up to a given value

List a set or list ref; changes from set to list if required.

Suitable small size for hash modules.

Weight of SO atoms when comparing, defaults to 1.

Compute the QBF equivalent to the given SO formula on the given structure.

Sobel differential operator.

Scharr differential operator.

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

Inline and solve fixed-points in the definitions.

Set the solver to use.

Constructors and unConstructors.

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

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

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

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 a string on characters satisfying f.

Look for characters from the list l after c, split on such pairs.

Split a string on empty lines (\n\n).

Split a string on newlines (\n or \r).

Split the formula as above and simplify by replacing trivially true or false atoms such as L(x:R) ...

Split a string on spaces.

Lexer for terms and types in internal format, to list

Another name for sprint.

Another name for sprint_def.

Another name for sprint_defs.

Print a picture in the simple PPM format to a string.

Print the structure in extensive form.

For the rules of the game, also print their compiled forms.

State in the given node.

Print the whole state: the game, structure, time and aux data.

Partition relations into static (not depending, even indirectly, on "true") and remaining ones.

A full one step of the computation.

Print a reduction

Game tree printing function.

Print a rule to string.

Print a regular structure class as a string, using its definition.

Print a polynomial as a string.

Print the given set as string.

Print the given assignment as string.

Print the structure struc as string.

Print the bit vector to string.

Print to formatter.

Print a formula as a string.

Abstract tree printing function.

Checks whether the first argument contains the second one.

Print definition to formatter.

Print definitions to formatter.

Index of the first occurence of the first argument in the second one.

Substitute all ocurrences of the first argument by the second one.

Substitute all ocurrences of the interval between the first argument and the second one by the third one.

Substitute the first ocurrence of the first argument by the second one.

Substitute the first ocurrence of the interval between the first argument and the second one by the third one.

Return the string representation of the given big integer, in decimal (base 10).

Strip characters satisfying f from left and right of a string.

Strip spaces from left and right of a string.

Parse the TRS string, output messages and the resulting structure.

Print a class definition (right hand side) as string.

Subtraction.

Substitute for variables in a QBF.

Substitute module variables.

Find a substitution for v which avoids avs.

Find a substitution for v which avoids avs, string arguments.

Prefix for variable name replacements.

Substitute once relations in defs by corresponding subformulas (with instantiated parameters).

Substitute a real variable with a subexpression.

Substitute recursively relations defined in defs by their definitions.

Apply substitution subst to all free variables in the given formula checking for and preventing name clashes with quantified variables.

Suffix all type variables, useful for renaming.

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 of two assignments, assuming that elems are all assignable elements.

QBF saying if the sum of signed numbers (lower-endian) is > 0.

Head symbol, i.e.

Get syntax definitions from a TRS.

We check that relations and SO variables appear with unique arities and that fixed-point variables appear only positively.

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

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

A flag whether to use the TC operator or not.

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.

Find a upto-n-step transitive closures of two-variable ?positive atomic formulas that hold on all pos_strucs and on no neg_strucs.

Maximum n between from and upto such that n-step TC of phi holds.

A helper function returning type with level indication, or ?t.

All paths in a term pointing to subterms that satisfy a predicate.

Concise readable form.

Convert formula to TNF; or negTNF when neg is set.

first existentially quantifies free vars

Helper function - put a list into an array of length k, pad with false, return whatever is left over.

Convert an arbitrary boolean combination to CNF.

Casts to particular variable types.

Convert an arbitrary boolean combination to DNF.

The list of set bits.

The list of set bits, in reverse order.

Reduction from top.

Sat check by reduction from top.

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

Translate a disjunction of conjunctions of literals (and disjs of lits).

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.

Transpose a rectangular matrix represented by lists.

Flatten and perform trivial simplifications (e.g.

Trivial simplification of Boolean definitions.

Apply TRS values to a structure.

List all tuples the first-order assignment asg assigns to vars in order in which vars are given.

Game tree unfolding.

Abstract game tree unfolding function, calls argument functions for work.

Maximax by depth unfolding function.

Maximax unfolding upto iterations, keep previous moves for stability.

Un-hash-cons a formula.

Un-hash-cons a real expression.

Match terms on the left to ground terms on the right, ignoring Const "_BLANK_" on the right.

Helper function: list of unique qbfs from l, in unspecified order.

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

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

Return the list of structurally unique elements, in order sorted by Pervasives.compare.

The big integer 1.

Project assignments on a given universal variable.

Remove parse level information from the head of the term.

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.

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

QBF saying if one number (unsigned lower-endian) is greater that another.

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

Whether to use DNF or TC=sums as gates in convolution.

Print a variable list as a string.

We recognize if the variable is FO (x), MSO (X), SO (|x) or Real (:x).

Print a variable as a string.

Helper function: apply subsutitution subst to the variable v.

List variables in the given polynomial.

All variables in a diagram, with the number of path they appear on.

List variables in the given polynomial list.

Simply set this array to the weights of integers in your diagrams.

The big integer 0.