## 2 Description

### 2.1 Basic features

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`".

### 2.2 Advanced features

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 6.3, 7).