next up previous contents
Next: Manipulators Up: Canonical form Previous: File Header   Contents

Boolean functions

A Boolean function may be expressed two ways:


<variable>
<function-identifier> ( arg1 arg2 ... )


where <function-identifier> is one of the following predefined function identifiers, and arg# is either a variable, a Boolean function or a reference to a Boolean function. The token <variable> is a character string and its use in an input file creates a simple Boolean function which is identified by that name, the value of which is the value of the variable named <variable>. Every Boolean function is implemented as a BDD (see Section [*]) and may have value T, or F, or have no value, depending on its arguments: values of Boolean functions are given as follows for each <function-identifier>.

Remark: Most functions take an arbitrary number of arguments, hence, parenthesis are necessary. Commas are considered whitespace and are ignored, however, their use is recommended to enhance the human readability of input files.

VAR


$\textstyle \parbox{110mm}{
Variables may be defined as Boolean functions using ...
...$' refer to previously defined functions or
manipulators instead of variables.}$

NOT


$\textstyle \parbox{110mm}{
The unary Boolean function {\tt NOT} has a value eq...
...ace of {\tt NOT} (functions cannot be complemented in
this way). Examples are:}$


not(x32)
-x32

ITE


$\textstyle \parbox{110mm}{
The ternary Boolean function {\tt ITE} has the value...
...first argument has value {\em F}.
Examples of this function are the following:}$


ite(ite( x3, $5, -x5), x4, x7)

AND


$\textstyle \parbox{110mm}{
This Boolean function has value {\em T} if all its ...
... at least one argument has value {\em F}.
Examples of its use are as
follows:}$


and(x1, x2, x3, x4)
and(-x1,
   and(x2, x3, $4),
   x5, $6, x7)

NAND


$\textstyle \parbox{110mm}{
This Boolean function has value {\em F} if all its a...
...ue
{\em T} and has value {\em T} if at least one argument has value {\em F}.
}$

OR


$\textstyle \parbox{110mm}{
This Boolean function has value {\em F} if all its a...
...lue
{\em F} and has value {\em T} if at least one argument has value {\em T}.
}$

NOR


$\textstyle \parbox{110mm}{
This Boolean function has value {\em T} if all its a...
...ue
{\em F} and has value {\em F} if at least one argument has value {\em T}.
}$

XOR


$\textstyle \parbox{110mm}{
This Boolean function has value {\em F} if an even number of its arguments
have value {\em T} and has the value {\em T} otherwise.}$

EQU


$\textstyle \parbox{110mm}{
This Boolean function has value {\em T} if an even n...
...{\em F} and has the value {\em F} otherwise. This is the negation
of {\tt XOR}}$

SAME


$\textstyle \parbox{110mm}{
This Boolean function has value {\em T} if all of it...
...he
same value, either {\em T} or {\em F}, and has the value {\em F} otherwise.}$

IMP


$\textstyle \parbox{110mm}{
As a binary Boolean function, {\tt imp} has value {\...
...r instance, {\tt imp(x1, x2, x3)} is equivalent to {\tt imp(imp(x1,
x2), x3)}.}$

NIMP


$\textstyle \parbox{110mm}{
As a binary Boolean function, {\tt imp} has value {\...
...nstance, {\tt nimp(x1, x2, x3)} is equivalent to {\tt nimp(nimp(x1, x2),
x3)}.}$


next up previous contents
Next: Manipulators Up: Canonical form Previous: File Header   Contents
John Franco 2011-09-15