   ## 5  Logical expressions

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 ";"!

### 5.1  Boolean operators

#### false

(or "0") always-false function.

#### true

(or "1") always-true function.

#### ident

reference to an argument or a variable (depending on the current context).

#### not exp

(or "-exp") complement.

#### exp or exp

(or "exp + exp") disjunction.

#### exp and exp

(or "exp . exp") conjunction.

#### exp xor exp

(or "exp <> exp") exclusive or.

implication.

equivalence.

#### ite(exp,exp,exp)

functionnal "if then else"; "ite(f,g,h)" is equivalent to "f.g + -f.h".

#### forall identlistexp

universal quantifier.

#### exist identlistexp

existential quantifier.

#### # (exp-list)

at most one true in the list.

#### nor exp-list

none is true in the list.

#### xor (exp-list)

exactly one true in the list. Warning: xor (x1,x2,...,xi) is NOT "x1 xor x2 xor ... xor xi" (except for i=2).

### 5.2  Control operators

Those operators allow the user to control the way expressions are evaluated.

#### compare(exp,exp)

returns 1 (the always-true function) if the two expressions are logically equivalent, 0 (the always-false function) otherwise.

#### implies(exp,exp)

returns 1 if the first expression implies the second one, 0 otherwise.

#### cuts(exp,exp)

returns 1 if the intersection of the two expressions is not empty (i.e. their logical and is not 0), 0 otherwise.

#### if exp then exp else exp

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.

#### let ident := exp in exp

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 6.2 for details).

### 5.3  Bdd decomposition

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:

• root(f) is the least argument f actually depends on, according to the argument total order.
• neither high(f) nor low(f) depend on root(f)

See 6.4 for more details on Shannon decomposition and BDD.

#### root(exp)

the least argument which the expression depends on.

#### high(exp)

the "high" branch of the expression (i.e. the formula when the root-var is true).

#### low(exp)

the "low" branch of the expression (i.e. the formula when the root-var is false).

#### root(exp-list)

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.

#### supp(exp)

returns the "support" of the exopression, that is, the "or" of all arguments the formula depends on.

### 5.4  Simplification modulo care-set

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(exp,exp)

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

#### constrain(exp,exp)

(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 xdoes not depend on f.

N.B. The result is undefined if the second operand is 0.

### 5.5  Priorities

Expressions can be enclosed within parenthesis. Some priorities are used to resolve ambiguities:

• not, exist, forall,
• else
• and
• or
• => (right associative)
• =, xor (right associative)
• in

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));
```   