The tool uses a internal representation knowned as "signed binary decision diagrams" (SBDD). With this representation, a boolean function F and its negation ¬ F are (almost) represented by the same internal structure (they differ only on a boolean flag). With classic BDDs, the internal representation of F and ¬ F are disjoints. As a consequence, the cost of the negation is constant with SBDDs, since it is linear with classical BDDs. Moreover, it is known that this representation is always cheaper (in size and in time computation) than classical BDDs.
The calculator deals with several kinds of identifiers:
The way an identifier is interpreted (i.e. the identifier’s status) depends on the current context. Intuitively, at the top level, there is a global context, giving the status of arguments and global variables. The status of a global identifier is implicitly given by its first occurence: if it first appears in the left hand side of an assigment, the status is variable; if it first appears in an expression, the status is argument. One can type "list" to see the current global context :
>>x := a . b; x := a . b >>list parameters are: a b variables are: x
An argument cannot be re-used as a global variable; a variable, indeed, can be re-assigned:
>>a := x; can't assign "a", not a variable >>x := a + b; x := a + b
Arguments are globals, while the scope of variables can be restricted using the let ... in ... operator.
>>y := let z := c + d in z; y := c + d >>list --note that z has disappeared, but not c and d: arguments are: a b c d variables are: x y
If id is a variable, let id := ... shadows the current value of id:
>>y; c + d >>z := let y := (let y := e.f in y.g) in x + y; z := a + b + e.f.g >>y; c + d
Moreover, a local declaration shadows the status of the identifier:
>>a; a >>let a := e.f in a; e.f >>a; a
For the time being, no static verifications are made on user-defined functions. We can simply give the semantics for function calls: if the user has defined a function foo(i1, ..., ik) := exp;, then foo(e1, ..., en), where e1, ..., en are correct expressions, is a correct expression equivalent to:
let i1 := e1 in ... let in := en in exp;
In particular, a user-defined function may use free identifiers, but it is indeed quite dangerous: depending on the context call, those identifiers will be interpretted either as arguments, global variables, or even local variables of the current scope!
The bdd decomposition is a special case of Shannon decomposition, where the choice of the decomposition variable is forced by the actual bdd representation. The general Shannon decomposition does not depend on the bdd structure, and can be obtained using logical operators; for all variable x and function f, we have f = (x ∧ f1) ∨ (¬ x ∧ f0), where (in bddc syntax):
f1 := exist x (x.f); -- or better: f1 := constrain(f,x); f0 := exist x (-x.f); -- or better: f0 := constrain(f,-x);
By default, the tool prints the results in a disjunctive normal form (sum of "ands"). The idea is to make the result as "readable" as possible. The quality of the "result" dramaticaly depends on the internal order of the arguments. For example, depending on the order of its arguments, the expression "if A then B else C" can produce different (but equivalent) polynomials, such as "A.B + -A.C + B.C" or "B.A + -A.C". Indeed, the second form is "better" since it is more concise, but the problem of printing the simpliest polynomial equivalent to a given function is exponential. So, there is no guarantee on the "quality" of the print result.
The user can also prints the results in a conjonctive normal form (product of or’s). This is the dual of the first form.
The Reed-Muller normal form consists in expressing the boolean functions as polynomials in "and" and "xor" (the always-true function "1" is also necessary). This form is canonical (modulo the commutativity and associativity of the operators). For instance:
>>reed (if A then B else C); >>B.A <> A.C <> C >>reed (not A); >>A <> 1
This form is interesting (since it is canonical), but it can seem "strange" and unreadable for most people! Moreover, there is no "simple" relation between the size of the Reed-Muller form and a classical polynomial form: one form can be exponentially better or worse than the other:
>>A + B + C; A + B + C >>reed (A + B + C); A.B.C <> A.B <> A.C <> A <> B.C <> B <> C >>A <> B <> C; A.B.C + A.-B.-C + -A.B.-C + -A.-B.C >>reed (A <> B <> C); A <> B <> C