Index of values

Be cautious, it is not type safe (if you use Cudd.Vdd.nodes_below_level, etc...: you can try to retrieve a constant value of some type and () value of the background value will be treated as another type.

Decompose an abstract value

Internal, do not use !

Unsafe conversion from and to Mpfr.t.

Unsafe conversion from and to Mpq.t.

C printing function.

Raw (C) printing function.

Return resp.

Addition; returns the new registerm, the carry, and the overflow (for signed integers).

Add an element to the universe (initially belonging to its singleton)

Returns the symbol associated to the given string, after having possibly registered the string if it wasn't (in this case, the symbol is fresh symbol).

add x s returns a set containing all elements of s, plus x.

add x s returns a set containing all elements of s, plus x.

add x s returns a set containing all elements of s, plus x.

add x s returns a set containing all elements of s, plus x.

add x s returns a multiset containing all elements of s, plus x.

add x s returns a multiset containing all elements of s, plus x.

add x y m returns a map containing the same bindings as m, plus a binding of x to y.

add tbl x y adds a binding of x to y in table tbl.

add x s returns a set containing all elements of s, plus x.

Add a new binding to the current map and return the new map.

Add a new binding to the table.

Adding to an environment a set of integer and real variables.

Cudd_addPlus.

add t x adds x to t.

Perturbation.

Perturbation.

Add an hyperedge.

Add the array of generators to the abstract value (time elapse operator).

Add the array of generators to the abstract value (time elapse operator).

Declaration of a new type

Declaration of a new type

Addition without normalization (internal)

Add the set of variables, possibly normalize the environment and return the applied permutation (that should also be applied to expressions defined in this environment)

Add the set of variables, possibly normalize the environment and return the applied permutation (that should also be applied to expressions defined in this environment)

Add a vertex

addmap m1 m2 merges the two maps m1 and m2.

Cudd_addAgreement.

Calls the right append function depending on the options.

Append two lists

Appends the two lists.

Append the two lists.

Combine the two previous operations.

Cudd_bddApproxConjDecomp.

Cudd_bddIterConjDecomp.

approximate man abs alg perform some transformation on the abstract value, guided by the argument alg.

approximate man abs alg perform some transformation on the abstract value, guided by the argument alg.

return the APRON sub-environment

Returns the arity of the local cache.

Returns the arity of the hashtable

Print an array

Change the environement of the array of constraints for a super-environement.

Change the environement of the array of generators for a super-environement.

Change the environement of the array of constraints for a super-environement.

Side-effect version of the previous function

Side-effect version of the previous function

Side-effect version of the previous function

Get the element of the given index (which is not a copy)

Get the element of the given index (which is not a copy)

Get the element of the given index (which is not a copy)

Get the environment of the array

Get the environment of the array

Get the size of the array

Get the size of the array

Get the size of the array

Make an array of tree expression constraints with the given size and defined on the given environement.

Make an array of generators with the given size and defined on the given environement.

Make an array of linear constraints with the given size and defined on the given environement.

Print an array of constraints

Print an array of generators

Print an array of constraints

Set the element of the given index (without any copy).

Set the element of the given index (without any copy).

Set the element of the given index (without any copy).

Assignement

Assignement

Parallel assignement of an array of dimensions by an array of same size of linear expressions

Parallel assignement of an array of dimensions by an array of same size of linear expressions

Assignement

Assignement

Parallel assignement of an array of dimensions by an array of same size of tree expressions

Parallel assignement of an array of dimensions by an array of same size of tree expressions

Create a list element from a single element.

attrhedge graph hedge returns the information associated to the hyperedge hedge

attrvertex graph vertex returns the information associated to the vertex vertex

Cudd_ReorderingStatus.

Cuddaux_addIte/Cudd_addIte.

Make a bdd manager from an underlying BDDAPRON manager

Make a bdd manager from an underlying BDDAPRON manager

Cudd_BiasedOverApprox.

Cudd_BiasedUnderApprox.

Return the list of all bindings of the given map.

Cudd_bddBooleanDiff.

Basic constructor

Create a bottom (empty) value defined on the given environment

Create a bottom (empty) value with the given number of integer and real variables

Top and bottom intervals (using DOUBLE coefficients)

Return the interval of variation of the dimension in the abstract value.

Return the interval of variation of the linear expression in the abstract value.

Return the interval of variation of the linear expression in the abstract value.

Return the interval of variation of the tree expression in the abstract value.

Return the interval of variation of the tree expression in the abstract value.

Return the interval of variation of the variable in the abstract value.

Canonicalize an abstract value by ensuring uniqueness and disjointness properties.

Canonicalize an abstract value by ensuring uniqueness and disjointness properties.

Put the abstract value in canonical form.

Put the abstract value in canonical form.

Return the number of elements of a set.

Return the number of elements of a set.

Return the number of elements of a set.

Return the number of elements of a set.

Return the number of elements of a multiset.

Return the number of elements of a multiset.

Number of keys of a map

Return the number of elements of a set.

Return the number of bindings.

Return the number of bindings.

The first parameter holds the quotient.

The first parameter holds the quotient.

The first parameter holds the quotient.

The two first parameters hold resp.

The two first parameters hold resp.

The first parameter holds the remainder.

The first parameter holds the remainder.

The first parameter holds the remainder.

Decomposition of the graph into Strongly Connected Components,

idem, but from several initial vertices.

Assuming a transformation for add_dimensions, invert it in-place to obtain the inverse transformation using remove_dimensions

Change of environments and renaming

Change the environement of the abstract values.

Checking function: raises Failure if problem, returns true otherwise.

Cudd_CheckKeys.

Prints error message and returns false if not normalized

Checking function: raises Failure if problem, returns true otherwise.

Return one element of the given set, or raise Not_found if the set is empty.

Return one element of the given set, or raise Not_found if the set is empty.

Return one element of the given set, or raise Not_found if the set is empty.

Return one element of the given set, or raise Not_found if the set is empty.

Return one element of the given multiset, or raise Not_found if the multiset is empty.

Return one element of the given multiset, or raise Not_found if the multiset is empty.

Returns a binding, or raise Not_found if empty

Return one element of the given set, or raise Not_found if the set is empty.

Clear all the conditions (results in a normalized environments)

Remove all vertices and hyperedges of the graph.

Empty a hash table.

Clear a table

Remove all elements from the table.

Clears the content of the local cache.

Clears the content of the hashtable

Clears the content of all created hashtables

Cudd_bddClippingAnd.

Cudd_bddClippingAndAbstract.

Closure: transform strict constraints into non-strict ones.

Closure: transform strict constraints into non-strict ones.

Side-effect version

Side-effect version

Non Total Comparison: If the 2 coefficients are both scalars, corresp. to Scalar.cmp, If the 2 coefficients are both intervals, corresp. to Interval.cmp, otherwise, -3 if the first is a scalar, 3 otherwise

Non Total Comparison: 0: equality -1: i1 included in i2 +1: i2 included in i1 -2: i1.inf less than or equal to i2.inf +2: i1.inf greater than i2.inf

Compare two coefficients, possibly converting to Mpqf.t.

Compare a coefficient with an integer

Return the code associated to the label

Evaluate the expression.

Evaluate the expression.

Evaluate the expression.

Evaluate the expression.

Evaluate the expression.

Evaluate the expression.

Evaluation

Cudd_Cofactor.

cofactor mtbdd cube evaluates mtbbdd on the cube cube

cofactor mtbdd cube evaluates mtbbdd on the cube cube

Cudd_Cofactor.

Returns the positive and negative cofactor of the ADD wrt the variable

Returns the positive and negative cofactor of the MTBDD wrt the variable

Returns the positive and negative cofactor of the MTBDD wrt the variable

Returns the positive and negative cofactor of the BDD wrt the variable

combineexpansive ~default ~merge (guard,leaf) vdd = merge (Vdd.ite guard leaf default) vdd.

Generic function, instanciated above.

Generic function, instanciated above.

Functions similar to combineleaf_array, but in which the first (resp.

Generic function,.

combinetractive (guard,leaf) vdd = Vdd.ite guard leaf vdd.

common commondata a b returns a map the keys of which must be keys in both a and in b, and those keys are bound to interdata d1 d2.

Return the common bindings.

Same as common, but the function receives as arguments the key (of the first map)

Comparison (do not correspond at all to alphabetic order, depend on the registration order of names in the module)

Total ordering between sets.

Total ordering between sets.

Total ordering between sets.

Total ordering between sets.

Total ordering between multisets.

Total ordering between multisets.

Total ordering between sets.

Compare two environment.

Comparison function

Comparison with lexicographic ordering using Coeff.cmp, terminating by constant

Comparison

Comparison function between maps, total if the comparison function for data is total

Compose an abstract value

Cuddaux_addCompose/Cudd_addCompose.

Cudd_bddCompose.

Default merge is List.rev_append

"Merge" is list cons

conjunction_of_minterm of_idb minterm translates a minterm into an explicit conjunction of type 'a Normalform.conjunction, using the function of_idb to produce elements of type 'a.

Calls the right cons function depending on the options.

Adding a new list element at the begining of the list

Performs the join of a list with an element.

Performs the join of a list with an element.

Cudd_bddConstrain.

Copy

Copy

Copy an hypergraph, using the given functions to duplicate the attributes associated to the elements of the graph.

Return a copy of the given hashtable.

Copy a value

Copy (deep copy)

Copy

Copy (deep copy)

Copy (deep copy)

Copy

Copy a value

Copy a tree expression constraint (deep copy)

Copy

Copy a generator (deep copy)

Copy a linear constraint (deep copy)

Copy

Internal use: duplicate a block to the major heap.

Cudd_bddCorrelation.

Cudd_bddCorrelationWeights.

Count the number of elements in the table.

Create a new universe set

create n data creates an hypergraph, using n for the initial size of internal hashtables, and data for the user information

create n creates a new, empty hash table, with initial size n.

Create a new table, with the specified initial size

create n creates a new empty weak hash table, of initial size n.

create ~size:n arity create a hashtable of arity arity, of the optional size n

Creates local caches of the given arity, with initial size size and maximal size maxsize.

Cudd_addConst.

Same as Cudd.Bdd.cube_of_bdd, but keep only the the values of variables having a determinated value.

Same as Cudd.Bdd.cube_of_bdd, but keep only the the values of variables having a determinated value.

Cudd_FindEssential.

Cudd_CubeArrayToBdd.

Split a cube into a cube of Booleans and a cube of conditions

Cuddaux_bddCubeUnion.

Cudd_bddAnd.

Cudd_DebugCheck.

Decompose an abstract value

Decompose a BDD f into a disjunction [(f1,g1);...;(fN,gN)] such that all decisions in f1...fN are Boolean variables;, all decisions in g1...gN are (non-Boolean) conditions;, f1...fN are pairwise disjoint.

Dual version

Internal use, look at the code.

Same for an array of BDDs/VDDs

Decompose a BDD/MTBDD into a tree with decisions on conditions, and purely Boolean BDDs on leaves

Cudd_E.

Returns the negative subnode of the MTBDD

Returns the negative subnode of the MTBDD

Cudd_E.

Cudd_Density.

Cudd_Density.

Return the (maximal) depth of the list.

Obsolete, moved in Bdd.Decompose

Returns the false BDD

Union, intersection and set difference.

Union, intersection and set difference.

Union, intersection and set difference.

Union, intersection and set difference.

Union, intersection and multiset difference.

Union, intersection and multiset difference.

Set difference.

Cudd_addDiff.

Union, intersection and multiset difference with a set.

Union, intersection and multiset difference with a set.

interset map set removes the bindings of a whose key belongs to set.

Remove the two-way bindings x <->y with x in the set

Remove the two-way bindings x <->y with y in the set

Return the dimension associated to the given variable in the environment.

dimchange e1 e2 computes the transformation for converting from an environment e1 to a superenvironment e2.

dimchange2 e1 e2 computes the transformation for converting from an environment e1 to a (compatible) environment e2, by first adding (some) variables of e2 and then removing (some) variables of e1.

Return the dimension of the environment

Cudd_AutodynDisable.

Default merge is List.rev_append

"Merge" is list cons

Cudd_addDivide.

Converts a BDD into a disjunctive normal form.

Cudd_Not.

not, and and or (use of 'd' prefix because of conflict with OCaml keywords)

not, and and or (use of 'd' prefix because of conflict with OCaml keywords)

not, and and or (use of 'd' prefix because of conflict with OCaml keywords)

not, and and or (use of 'd' prefix because of conflict with OCaml keywords)

not, and and or (use of 'd' prefix because of conflict with OCaml keywords)

not, and and or (use of 'd' prefix because of conflict with OCaml keywords)

Cudd_bddOr.

Cudd_T.

Returns the positive subnode of the MTBDD

Returns the positive subnode of the MTBDD

Cudd_T.

Returns the true BDD

Cudd_V.

Returns the value of the assumed constant MTBDD

Returns the value of the assumed constant MTBDD

Return the list of all elements of the given set.

Return the list of all elements of the given set.

Return the list of all elements of the given set.

Return the list of all elements of the given set.

Return the list of all elements of the given multiset.

Return the list of all elements of the given multiset.

Return the list of all elements of the given set.

The empty set.

The empty set.

The empty set.

The empty set.

The empty multiset.

The empty multiset.

The empty map.

The empty set.

Empty map

Cudd_AutodynEnable.

Same as nxor

Equality operation

Same as nxor

Equality operation

Under which condition are the expressions equal ? In case of arithmetic expressions, do not take into account the careset.

Under which condition are the expressions equal ? In case of arithmetic expressions, do not take into account the careset.

Same as nxor

Equality operation

Same as nxor

Equality operation

Same as nxor

Equality operation

Same as nxor

Equality operation

Same as Cudd.Bdd.nxor

Under which condition the 2 registers are equal ?

Equality test.

Equality test

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal s1 s2 tests whether the multisets s1 and s2 are equal, that is, contain equal elements with equal occurence numbers.

equal s1 s2 tests whether the multisets s1 and s2 are equal, that is, contain equal elements with equal occurence numbers.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

The equality predicate used to compare keys.

Test equality if two environments

Equality test

Equality test

Equality test, possibly using a conversion to Mpqf.t.

Is the coefficient equal to scalar b or interval b,b ?

Is the interval equal to i,i ?

Equality test with an integer

Under which condition the register is equal to the label ?

equality between maps

Escape a string, replacing line breaks by linebreak (default '\n').

Cuddaux_addEvalConst/Cudd_addEvalConst.

Variation of Cudd_addExistAbstract.

Cudd_bddExistAbstract.

Cudd_bddAndAbstract.

Is the string already registered ?

exists p s checks if at least one element of the set satisfies the predicate p.

exists p s checks if at least one element of the set satisfies the predicate p.

exists p s checks if at least one element of the set satisfies the predicate p.

exists p s checks if at least one element of the set satisfies the predicate p.

Existence test

exists p s checks if at least one element of the set satisfies the predicate p.

Cudd_bddXorExistAbstract.

Expansion: expand a var tvar expands the variable var into itself and the additional variables in tvar, which are given the same type as var.

Expansion: expand a dim n expands the dimension dim into itself + n additional dimensions.

Same as above, but with \/ replaced by merge (supposed to be commutative and associative).

Same as above, but with \/ replaced by merge (supposed to be commutative and associative).

register extension or truncation.

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

extend_environment permute value env embed value in the new (super)environment env, by computing the permutation transformation and using permute to apply it to the value.

Change the environement of the constraint for a super-environement.

Change the environment of the expression for a super-environement.

Change the environement of the generator for a super-environement.

Change the environement of the constraint for a super-environement.

Change the environment of the expression for a super-environement.

Side-effect version of the previous function

Side-effet version of the previous function

Side-effect version of the previous function

Side-effect version of the previous function

Side-effet version of the previous function

Extract the list of sets

Dump on the stdout C stream the internal representation of an abstract value, for debugging purposes

Dump on the stdout C stream the internal representation of an abstract value, for debugging purposes

filter p s returns the set of all elements in s that satisfy predicate p.

filter p s returns the set of all elements in s that satisfy predicate p.

filter p s returns the set of all elements in s that satisfy predicate p.

filter p s returns the set of all elements in s that satisfy predicate p.

filter p l returns all the elements of the multiset l that satisfy the predicate p.

filter p l returns all the elements of the multiset l that satisfy the predicate p.

filter p m returns the map of all bindings in m that satisfy predicate p.

filter p s returns the set of all elements in s that satisfy predicate p.

find x m returns the current binding of x in m, or raises Not_found if no such binding exists.

find tbl x returns the current binding of x in tbl, or raises Not_found if no such binding exists.

find t x returns an instance of x found in t.

find_all tbl x returns the list of all data associated with x in tbl.

find_all t x returns a list of all the instances of x found in t.

Flatten the recursive list, only starting from the given

cuddCacheFlush.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

fold f s a computes (f (xN,On) ... (f (x2,O2) (f (x1,o1) a))...), where (x1,o1) ... (xN,oN) are pairs of elements of s with their occurence number.

fold f s a computes (f (xN,On) ... (f (x2,O2) (f (x1,o1) a))...), where (x1,o1) ... (xN,oN) are pairs of elements of s with their occurence number.

fold f m a computes (f kN dN ... (f k1 d1 a)...), where k1 ... kN are the keys of all bindings in m, and d1 ... dN are the associated data.

fold f tbl init computes (f kN dN ... (f k1 d1 init)...), where k1 ... kN are the keys of all bindings in tbl, and d1 ... dN are the associated values.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

Iterate on bindings and accumulating a result.

Iterate on bindings and accumulating a result.

Folding: fold a tvar fold the variables in the array tvar of size n>=1 and put the result in the first variable of the array.

Folding: fold a tdim fold the dimensions in the array tdim of size n>=1 and put the result in the first dimension of the array.

fold f t init computes (f d1 (... (f dN init))) where d1 ... dN are the elements of t in some unspecified order.

Idem as List.fold_X functions

Idem as List.fold_X functions

Idem as List.fold_X functions

Idem as List.fold_X functions

Ordinary fold function for atoms, from left to right.

Ordinary fold function for atoms, from right to left.

for_all p s checks if all elements of the set satisfy the predicate p.

for_all p s checks if all elements of the set satisfy the predicate p.

for_all p s checks if all elements of the set satisfy the predicate p.

for_all p s checks if all elements of the set satisfy the predicate p.

for_all p s checks if all elements of the set satisfy the predicate p.

Variation of Cudd_addUnivAbstract.

Cudd_bddUnivAbstract.

Forget (existential quantification) a list of variables

Forget (existential quantification) a list of variables

Forget (existential quantification) a list of variables

Eliminating variables

Eliminating variables

Eliminating variables

Eliminating variables

Return the default options for any function (0 or false for al fields)

cuddGarbageCollect.

Cudd_bddGenDisjDecomp.

Cudd_bddVarConjDecomp.

Conversion from lexing buffers to resp.

Conversion from lists of strings to array of resp.

Conversion from strings to resp.

Type conversion (no computation)

Type conversion (no computation)

Cudd_ReadArcviolation.

Cudd_ReadBackground.

Cudd_ReadSize.

Cudd_ReadCacheHits.

Cudd_ReadCacheLookUps.

Cudd_ReadCacheSlots.

Cudd_ReadCacheUsedSlots.

Get the coefficient of the variable in the underlying linear expression

Get the coefficient of the variable in the underlying linear expression

Get the coefficient of the variable

Get the coefficient corresponding to the dimension

Extract resp.

Extract resp.

Extract resp.

Cudd_ReadNumberXovers.

Get the constant of the underlying linear expression

Get the constant

Get the constant

Cudd_ReadDead.

Get the environement of the tree expression constraint

Get the environement of the expression

Get the environement of the generator

Get the environement of the linear constraint

Get the environement of the expression

Cudd_ReadEpsilon.

Cudd_ReadErrorCode.

Get the corresponding result flag

Get the corresponding result flag

Get the options sets for the function.

Cudd_ReadGarbageCollections.

Cudd_ReadGarbageCollectionTime.

Get the underlying generator of level 0.

Cudd_ReadGroupcheck.

Cudd_ReadKeys.

Get the name of the effective library which allocated the manager

Get the underlying linear constraint of level 0.

Cudd_ReadLinear.

Get the underlying expression of level 0 (which is not a copy).

Get the underlying linear expression.

Get the underlying linear expression.

Cudd_ReadLooseUpTo.

Cudd_ReadMaxCache.