The bddc utility implements an interactive processor for the evaluation of logical formula. It reads commands from the standard input, and prints the result to the standard output. The main commands are those which involve Boolean expressions: basically, bddc computes a bdd (binary decision diagram [1, 2]), which is a canonical representation of the expression.
For instance, if the user types the expression "x + y.z ;", the calculator interprets symbols x, y and z as Boolean arguments (i.e., basic propositions), and the whole expression as a Boolean function over those arguments. Note that "+" stands for logical or, and "." operator for logical and. The calculator builds the bdd corresponding to the expression, and then prints a polynomial representation of this canonical form; in the example, it simply outputs "x + y.z" (useful, isn’t it?).
If the expression is a tautology, its bdd is the always-true function: for instance, if the user types "x => (y => x);" (=> is the logical implication), the result is "true".
The user may assign an expression to a variable, and then use this variable to build a new expression (">>" is the prompt symbol of the processor):
>>f := (y => x); x + -y >>x => f; true
Moreover, the user may define new operators on bdds. For instance :
>>union(A, B) := A + B; --new function: union, arity: 2 >>union(x.y, t); x.y + t
Indeed, this example is quite stupid. Defining new operators becomes interesting when using control operators and recursion (see 5.3, 6).