The calculator provides all the classical Boolean operators, plus some other specially dedicated to the bdd implementation. The syntax is infixed, and the expression can be typed on more than one line, so don’t forget the terminating symbol ";"!
(or "0") always-false function.
(or "1") always-true function.
reference to an argument or a variable (depending on the current context).
(or "-exp") complement.
(or "exp + exp") disjunction.
(or "exp . exp") conjunction.
(or "exp <> exp") exclusive or.
implication.
equivalence.
functionnal "if then else"; "ite(f,g,h)" is equivalent to "f.g + -f.h".
universal quantifier.
existential quantifier.
at most one true in the list.
none is true in the list.
exactly one true in the list. Warning: xor (x1,x2,...,xi) is NOT "x1 xor x2 xor ... xor xi" (except for i=2).
Those operators allow the user to control the way expressions are evaluated.
returns 1 (the always-true function) if the two expressions are logically equivalent, 0 (the always-false function) otherwise.
returns 1 if the first expression implies the second one, 0 otherwise.
returns 1 if the intersection of the two expressions is not empty (i.e. their logical and is not 0), 0 otherwise.
lazy "if": if the first operand is always-true (resp. always-false), the second (resp. third) operand is not evaluated; otherwise, it behaves as the ite operator.
local variable definition : the first expression is evaluated in a new context where ident is undefined. Then, the second expression is evaluated in a new context where the first result is associated to ident. The original context is then restaured, and the second result is returned (see 5.2 for details).
The following operators are specific to the bdd representation: in particular, they do depend on the internal order of the arguments.
Every formula "f" that actually depends on at least one argument (i.e. neither 0 nor 1) is equivalent to "f = if root(f) then high(f) else low(f)", where:
See 5.4 for more details on Shannon decomposition and BDD.
the least argument which the expression depends on.
the "high" branch of the expression (i.e. the formula when the root-var is true).
the "low" branch of the expression (i.e. the formula when the root-var is false).
when called with more than one argument, the root function returns the minimal root-var of all the expressions. This generalisation is quite useful when defining recusive functions on the bdd stucture.
returns the "support" of the exopression, that is, the "or" of all arguments the formula depends on.
The following operators are specific to the bdd representation: in particular, they do depend on the internal order of the arguments.
It is often the case that a particular formula is manipulated under a set of assumptions, or "care-set".
"restrict(f,g)" is a function equivalent to "f" if "g"; the result is simplier than "f" (less bdd nodes). The result is a function h satisfying:
| if (f ∧ g = 0) then h = 0 |
| if (f ∨ ¬ g = 1) then h = 1 |
Otherwise, h is some function satisfying:
| (f ∧ g) ⇒ h ⇒ (f ∨ ¬ g) |
N.B. The result is undefined if the second operand is 0.
(also called the generalized cofactor) is a kind of "restrict" operation. The result is not garanted to be "smaller" than f, but it has an interesting (but not trivial) property: let h = constrain(f,g)
| h(x) = f(x′) where x′ = "the closer point to x in g" |
The precise definition of the "closer point ..." function is a little bit complicated (and depends on the variable ordering), but the main result is that the choice of x′ does not depend on f.
N.B. The result is undefined if the second operand is 0.
Expressions can be enclosed within parenthesis. Some priorities are used to resolve ambiguities:
For instance:
let z := t = v in - exist x if y then x else z + z = y => z ;
is interpreted as:
let z := (t = v) in ((- (exist x (if y then x else z)) + z) = (y => z));