Index of values

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

Clear the database

Return the code associated to the label

Tests

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

Under which condition the 2 registers are equal ?

Equality test.

Under which condition the register is equal to the label ?

Existential quantification of a set of variables

register extension or truncation.

Universal quantification of a set of variables

Signed strictly-greater-than test.

Signed greater-or-equal test.

Return the guard of the integer value in the BDD register.

Return the guard of the integer value in the BDD register.

Return the guard of the label in the BDD register.

Return the guard of the deterministic minterm in the BDD register.

Return the list g -> n represented by the BDD register.

Return the list g -> n represented by the BDD register.

Return the list g -> label represented by the BDD register.

Unsigned strictly-greater-than test.

Tests w.r.t.

Unsigned greater-or-equal test.

Output the IDD and return its identifier

info associated to the variable in db

Does the register contain a constant value ?

Tests whether it contains a constant value.

Is the minterm completely non-determinated ? (ie, contain only undefined values)

If-then-else operation

If-then-else operator.

if-then-else operation.

Iter the function on all label of the given type contained in the minterm.

Iterate the function on all the integer values represented by the argument minterm.

Iterate the function on all determinated minterms represented by the argument minterm.

Iterate on definitions of BDD identifiers, in a topological order.

Iterate the function on all the registered conditions

Iterate the function on all the registered conditions, from level 0 to higher levels.

Iterate on definitions of IDD identifiers, in a topological order.

Iter on all variables declared in the database

Return the label associated to the given code interpreted as of type the given type.

Return the array of labels defining the type

Logical negation (for all bits).

Create a database for printing BDDs/IDDs.

Raises Exit if false value

Apply the function to all label of the given type contained in the minterm and return the list of the results.

Apply the function to all integer values represented by the argument minterm and return the list of the results.

Apply the function to all determinated minterms represented by the argument minterm and return the list of the results.

Return the maximal integer corresponding to a label belonging to the type.

Is the BDD index managed by the database ?

Does the integer code some label of the given type ?

min_size cst computes the minimum number of bits required to represent the given constant.

Unary negation; be cautious, if the size of integer is n, the negation of -2^(n-1) is itself.

Convert a possibly negative integer into a minterm of size size

of_int size cst puts the constant integer cst in a constant register of size size.

Create a register of the type of the label containing the label

Predecessor operation; returns the new register and the carry.

print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

Print a BDD

Print the database

Print the database

Print an expression

Print the name associated to the single BDD index.

Print the condition

Print the condition represented by the signed BDD index.

Print an IDD, using the function to associate to leaf indices strings.

Print an object of type info

Print a minterm

print_minterm f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

print_minterm f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

print_minterm f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

Print a type

Print a type definition

Return the underlying array of BDD representing the expression

Variable renaming.

Multiplication by a positive constant.

shift_left man t n shifts the register to the left by n bits.

shift_right t n shifts the register to the right by n bits.

Same as shift_right, but here logical shift: a zero is always inserted.

Output the BDD and return its identifier

Return the cardinality of a type (the number of its labels)

Substraction; returns the new register, the carry, and the overflow (for signed integers).

Parallel substitution of variables by expressions

Successor operation; returns the new register and the carry.

Return the support of an expression as a conjunction of the BDD identifiers involved in the expression

Operations

Convert a constant register to its value as a code.

Convert a minterm to a (possibly signed) integer.

to_int sign x converts a constant register to an integer.

Convert a constant register to its value as a label.

Type of an expression

Expression representing the litteral var

Return the variable and info involved by the BDD index

Return the support of an array of expressions as a conjunction of the BDD identifiers involved in the expressions

Tests the register to zero.