Index of values


A
add [Formula.Arith]
add [Formula.Bint]
add [ArithDD]
add [Arith.Poly]
add [Arith.Lin]
add [Arith]
add [Bddint]
add [Bddreg]
Addition; returns the new registerm, the carry, and the overflow (for signed integers).

B
bddsupport [Bddvar]
bool_of_tbool [Bddvar.Expr]

C
cleanup [Formula]
clear_db [Bddoutput]
Clear the database
code_of_label [Bddenum]
Return the code associated to the label
cofactor [Formula]
cofactor [ArithDD]
cofactor [Bddvar]
compare [Arith.Condition]
compare [Arith.Poly]
compare [Arith.Lin]
compare [Arith]
compare_lterm [Arith.Lin]
compare_monomial [Arith.Poly]
compare_varexp [Arith.Poly]
compose [Bddvar]
compose_of_substitution [Formula]
composition_of_substitution [Bddvar]
compute_careset [CondDD]
cond_support [CondDD]
condition [Formula.Arith]
condition [ArithDD]
Tests
condition [CondDD]
conjunction_of_minterm [Bddvar.Expr]
cst [Formula.Arith]
cst [ArithDD]
cst [Arith.Poly]
cst [Arith.Lin]
cst [Arith]
cube_of_bdd [Bddvar]
Same as Bdd.cube_of_bdd, but keep only the the values of variables having a determinated value.

D
dand [Formula.Bool]
dfalse [Formula.Bool]
disjunction_of_bdd [Bddvar.Expr]
div [Formula.Arith]
div [ArithDD]
div [Arith.Poly]
div [Arith]
dnot [Formula.Bool]
dor [Formula.Bool]
dtrue [Formula.Bool]
dummy [Var]

E
eq [Formula.Arith]
eq [Formula.Benum]
eq [Formula.Bint]
eq [Formula.Bool]
eq [Formula]
eq [ArithDD]
eq_int [Formula.Bint]
eq_label [Formula.Benum]
equal [Arith]
equal [Bddenum]
Under which condition the 2 registers are equal ?
equal [Bddint]
equal [Bddreg]
Equality test.
equal_int [Bddint]
equal_int [Bddreg]
equal_label [Bddenum]
Under which condition the register is equal to the label ?
exist [Bddvar]
Existential quantification of a set of variables
exists [Formula.Bool]
extend [Bddint]
extend [Bddreg]
register extension or truncation.

F
forall [Formula.Bool]
forall [Bddvar]
Universal quantification of a set of variables

G
gmod [Formula.Arith]
gmod [ArithDD]
gmod [Arith]
greater [Bddint]
greater [Bddreg]
Signed strictly-greater-than test.
greater_int [Bddreg]
greatereq [Bddint]
greatereq [Bddreg]
Signed greater-or-equal test.
greatereq_int [Bddint]
greatereq_int [Bddreg]
guard_of_int [Bddint]
Return the guard of the integer value in the BDD register.
guard_of_int [Bddreg]
Return the guard of the integer value in the BDD register.
guard_of_label [Bddenum]
Return the guard of the label in the BDD register.
guard_of_minterm [Bddreg]
Return the guard of the deterministic minterm in the BDD register.
guardints [Bddint]
Return the list g -> n represented by the BDD register.
guardints [Bddreg]
Return the list g -> n represented by the BDD register.
guardlabels [Bddenum]
Return the list g -> label represented by the BDD register.

H
hash [Arith]
higher [Bddreg]
Unsigned strictly-greater-than test.
higher_int [Bddreg]
Tests w.r.t.
highereq [Bddreg]
Unsigned greater-or-equal test.
highereq_int [Bddreg]

I
idattr_of_idd [Bddoutput]
Output the IDD and return its identifier
info_of_var [Bddvar]
info associated to the variable in db
is_cst [Bddenum]
Does the register contain a constant value ?
is_cst [Bddint]
is_cst [Bddreg]
Tests whether it contains a constant value.
is_dependent_on_integer_only [Arith]
is_included_in [Formula.Bool]
is_indet [Bddreg.Minterm]
Is the minterm completely non-determinated ? (ie, contain only undefined values)
is_inter_empty [Formula.Bool]
ite [Formula.Arith]
ite [Formula.Benum]
ite [Formula.Bint]
ite [Formula.Bool]
ite [Formula]
ite [ArithDD]
ite [Bddvar]
If-then-else operation
ite [Bddenum]
If-then-else operator.
ite [Bddint]
ite [Bddreg]
if-then-else operation.
iter [Bddenum.Minterm]
Iter the function on all label of the given type contained in the minterm.
iter [Bddint.Minterm]
Iterate the function on all the integer values represented by the argument minterm.
iter [Bddreg.Minterm]
Iterate the function on all determinated minterms represented by the argument minterm.
iter_bdef_ordered [Bddoutput]
Iterate on definitions of BDD identifiers, in a topological order.
iter_cond [Bddoutput]
Iterate the function on all the registered conditions
iter_cond_ordered [Bddoutput]
Iterate the function on all the registered conditions, from level 0 to higher levels.
iter_idef_ordered [Bddoutput]
Iterate on definitions of IDD identifiers, in a topological order.
iter_ordered [Bddvar]
Iter on all variables declared in the database

L
label_of_typcode [Bddenum]
Return the label associated to the given code interpreted as of type the given type.
labels_of_typ [Bddenum]
Return the array of labels defining the type
lin_of_poly [Arith]
lin_of_tree [Arith]
lnot [Bddreg]
Logical negation (for all bits).

M
make [Arith.Condition]
make_db [Bddoutput]
Create a database for printing BDDs/IDDs.
mand [Bddvar.Expr]
Raises Exit if false value
map [Bddenum.Minterm]
Apply the function to all label of the given type contained in the minterm and return the list of the results.
map [Bddint.Minterm]
Apply the function to all integer values represented by the argument minterm and return the list of the results.
map [Bddreg.Minterm]
Apply the function to all determinated minterms represented by the argument minterm and return the list of the results.
maxcode_of_typ [Bddenum]
Return the maximal integer corresponding to a label belonging to the type.
mem_id [Bddvar]
Is the BDD index managed by the database ?
mem_typcode [Bddenum]
Does the integer code some label of the given type ?
min_size [Bddreg]
min_size cst computes the minimum number of bits required to represent the given constant.
mul [Formula.Arith]
mul [ArithDD]
mul [Arith.Poly]
mul [Arith]

N
nand [Formula.Bool]
neg [Formula.Bint]
neg [Bddint]
neg [Bddreg]
Unary negation; be cautious, if the size of integer is n, the negation of -2^(n-1) is itself.
negate [Formula.Arith]
negate [ArithDD]
negate [Arith.Condition]
negate [Arith.Poly]
negate [Arith.Lin]
negate [Arith]
nor [Formula.Bool]
normalize [Arith.Poly]
normalize [Arith.Lin]
normalize [Arith]
normalize_as_constraint [Arith.Poly]
normalize_as_constraint [Arith.Lin]
normalize_as_constraint [Arith]
normalize_full [Arith.Poly]
normalize_monomial [Arith.Poly]
nxor [Formula.Bool]

O
of_bool [Formula.Bool]
of_expr [Formula.Arith]
of_expr [Formula.Benum]
of_expr [Formula.Bint]
of_expr [Formula.Bool]
of_expr [ArithDD]
of_int [Formula.Bint]
of_int [Bddint]
of_int [Bddreg.Minterm]
Convert a possibly negative integer into a minterm of size size
of_int [Bddreg]
of_int size cst puts the constant integer cst in a constant register of size size.
of_label [Bddenum]
Create a register of the type of the label containing the label
other [Formula.Arith]
other [ArithDD]
other [Arith]

P
permutation_of_rename [Bddvar]
permute [Bddvar]
poly_of_tree [Arith]
pred [Formula.Bint]
pred [Bddint]
pred [Bddreg]
Predecessor operation; returns the new register and the carry.
print [Formula.Arith]
print [Formula.Benum]
print [Formula.Bint]
print [Formula.Bool]
print [ArithDD]
print [Arith.Condition]
print [Arith.Tree]
print [Arith.Poly]
print []
print [Arith]
print [Bddenum]
print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.
print [Var]
print [Bddint]
print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.
print [Bddreg]
print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.
print_bdd [Formula]
print_bdd [Bddvar]
Print a BDD
print_cond [Formula]
print_cond [CondDD]
print_conjunction [Bddvar.Expr]
print_db [Formula]
print_db [CondDD]
print_db [Bddvar]
Print the database
print_db [Bddenum]
Print the database
print_disjunction [Bddvar.Expr]
print_expr [Formula]
print_expr [Bddvar]
Print an expression
print_id [Bddvar]
Print the name associated to the single BDD index.
print_idcond [Bddvar]
Print the condition
print_idcondb [Bddvar]
Print the condition represented by the signed BDD index.
print_idd [Bddvar]
Print an IDD, using the function to associate to leaf indices strings.
print_info [Bddvar]
Print an object of type info
print_minterm [Bddvar]
Print a minterm
print_minterm [Bddenum]
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 [Bddint]
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 [Bddreg]
print_minterm f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.
print_term [Bddvar.Expr]
print_typ [Formula]
print_typ [CondDD]
print_typ [Arith]
print_typ [Bddvar]
Print a type
print_typdef [Formula]
print_typdef [CondDD]
print_typdef [Bddvar]
Print a type definition

R
reg_of_expr [Bddvar]
Return the underlying array of BDD representing the expression
rename [Arith.Tree]
rename [Arith.Poly]
rename [Arith.Lin]
rename [Arith]
rename [Bddvar]
Variable renaming.

S
scale [Formula.Bint]
scale [Arith.Poly]
scale [Arith.Lin]
scale [Bddint]
scale [Bddreg]
Multiplication by a positive constant.
shift_left [Formula.Bint]
shift_left [Bddint]
shift_left [Bddreg]
shift_left man t n shifts the register to the left by n bits.
shift_right [Formula.Bint]
shift_right [Bddint]
shift_right [Bddreg]
shift_right t n shifts the register to the right by n bits.
shift_right_logical [Bddreg]
Same as shift_right, but here logical shift: a zero is always inserted.
signid_of_bdd [Bddoutput]
Output the BDD and return its identifier
size_of_typ [Bddenum]
Return the cardinality of a type (the number of its labels)
sub [Formula.Arith]
sub [Formula.Bint]
sub [ArithDD]
sub [Arith.Poly]
sub [Arith.Lin]
sub [Arith]
sub [Bddint]
sub [Bddreg]
Substraction; returns the new register, the carry, and the overflow (for signed integers).
substitute [Formula]
substitute [Bddvar]
Parallel substitution of variables by expressions
substitute_cond [Formula.Arith]
substitute_cond [ArithDD]
substitute_ddexpr [CondDD]
substitute_expr [Formula.Arith]
substitute_expr [ArithDD]
succ [Formula.Bint]
succ [Bddint]
succ [Bddreg]
Successor operation; returns the new register and the carry.
sup [Formula.Arith]
sup [Formula.Bint]
sup [ArithDD]
supeq [Formula.Arith]
supeq [Formula.Bint]
supeq [ArithDD]
supeq_int [Formula.Bint]
support [Formula]
support [Arith.Condition]
support [Arith.Tree]
support [Arith.Poly]
support [Arith.Lin]
support [Arith]
support_cond [Formula]
support_cond [ArithDD]
support_cond [Bddvar]
Return the support of an expression as a conjunction of the BDD identifiers involved in the expression
support_leaf [ArithDD]

T
tdrestrict [Formula]
tdrestrict [ArithDD]
tdrestrict [Bddvar]
term_of_idcondb [Bddvar.Expr]
term_of_venum [Bddvar.Expr]
term_of_vint [Bddvar.Expr]
to_add [ArithDD]
Operations
to_code [Bddenum]
Convert a constant register to its value as a code.
to_expr [Formula.Arith]
to_expr [Formula.Benum]
to_expr [Formula.Bint]
to_expr [Formula.Bool]
to_expr [ArithDD]
to_int [Bddint]
to_int [Bddreg.Minterm]
Convert a minterm to a (possibly signed) integer.
to_int [Bddreg]
to_int sign x converts a constant register to an integer.
to_label [Bddenum]
Convert a constant register to its value as a label.
to_string [Var]
tree_of_lin [Arith]
tree_of_poly [Arith]
typ_of_expr [Formula]
typ_of_expr [Arith]
typ_of_expr [Bddvar]
Type of an expression

V
var [Formula.Arith]
var [Formula.Benum]
var [Formula.Bint]
var [Formula.Bool]
var [Formula]
var [ArithDD]
var [Arith.Poly]
var [Arith.Lin]
var [Arith]
var [Bddvar]
Expression representing the litteral var
varinfo_of_id [Bddvar]
Return the variable and info involved by the BDD index
vectorsupport_cond [Formula]
vectorsupport_cond [Bddvar]
Return the support of an array of expressions as a conjunction of the BDD identifiers involved in the expressions

X
xor [Formula.Bool]

Z
zero [Formula.Bint]
zero [Bddint]
zero [Bddreg]
Tests the register to zero.