Directives

The syntax of a directive is


<command> <arg>, ...


where <arg> are Boolean functions or manipulators or variables. The following are commands and a description of how they apply their arguments.

INITIAL_BRANCH


$\parbox{110mm}{ The directive {\tt INITIAL\_BRANCH} may be invoked ... ...search order has been revealed. An example of this directive is the following:}$


   initial_branch (x1, x39, x5, x4, x24, x3)


$\parbox{110mm}{ This marks variables $x_1$, $x_{39}$, $x_5$, $x_4$, ... ...means branch on all variables beginning with {\tt x3} and ending with {\tt 3}.}$

$\parbox{110mm}{ The order in which wild card variables are searched ... ... {\tt initial\_branch} directives in one. An example of this is the following:}$


   initial_branch (#1, x1, x39%20.5, x5)
   initial_branch (#2, x4, x24, x3%80.25)


$\parbox{110mm}{ This marks variables $x_1$, $x_{39}$, and $x_5$, to ... ... {\em False}, likewise $x_3$\ is more likely be assigned the value {\em True}.}$

#DEFINE


$\parbox{110mm}{ A rudimentary macro facility. The syntax is the following:}$


#define <pattern> # <Boolean-function>


$\parbox{110mm}{ where {\tt <pattern>} is a {\tt <function-identifier... ...{\tt <function-specifier>} must be arguments in {\tt <pattern>}. For example,}$


#define slide(x1, x17, x15, x33, x40)
#       equ(xor(x1, and(-x17, x33),ite(x15, or(x33, -x40), -x33)))


$\parbox{110mm}{ substitutes the {\tt e... ...luding built-in functions, may be redefined using {\tt \char93 define}. Thus,}$


#define and3(x, y, z) # or3(x, y, z)


$\parbox{110mm}{ causes three input {\tt and3} functions occurring {\... ...t \char93 define} to behave as three input {\tt or3} functions. A line such as}$


#define and3(x, y, z) # and(and(x, y), z)


$\parbox{110mm}{ redefines {\tt and3} to what it had been initially ... ...th an identical {\tt <function-identifier>}. For example, after the following:}$


#define and(x, y, z) # or3(x, y, z)
#define and(x, y, z, w) # or4(x, y, z, w)


$\parbox{110mm}{ The function {\tt and(x, y, z, w)} is defined but {\tt and(x, y, z)} is not.}$

PRINT_TREE


$\parbox{110mm}{ The PRINT\_TREE function takes one Boolean function,... ...anch is the $T$\ branch and the right branch is the $F$\ branch. For example,}$


print_tree(or3 (4, 5, -6))


$\parbox{110mm}{ prints the following to standard output: \par -{}-{}... ...}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}- }$


$\parbox{110mm}{ It is possible to control the variable ordering of t... ... ordering can be controlled by creating a dummy define statement, for example:}$


#define ordering(a, b, c, d) # or4(a, b, c, d)


$\parbox{110mm}{ This forces variable $a$\ to occur as or near the le... ...f printed trees, and $d$\ to occur as or near the root. For example, the lines}$


#define ordering(b, a, d, c) # or4(b, a, d, c)
print_tree(minmax(4, 1, 3, a, b, c, d))


$\parbox{110mm}{ prints the following to standard output (assuming $a... ...}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}- }$

PPRINT_TREE


$\parbox{110mm}{ Does the same thing as {\tt PRINT\_TREE} except the ... ...ical form with {\tt ite} used to indicate $T$\ and $F$\ branches. For example,}$


pprint_tree(or3 (4, 5, -6))


$\parbox{110mm}{ prints to standard output: \par -{}-{}-{}-{}-{}-{}-{... ...}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-~}$

PPRINT_XDD


$\parbox{110mm}{ Does a similar thing to {\tt PRINT\_TREE} except the output is shown in terms of nested ANDs and XORs. For example,}$


print_xdd(or3 (4, 5, -6))


$\parbox{110mm}{ prints to standard output: \par -{}-{}-{}-{}-{}-{}-{... ...}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-~}$

PPRINT_FLAT_XDD


$\parbox{110mm}{ Does the same thing as {\tt PRINT\_XDD} except the function is displayed in its unnested form. For example,}$


print_flat_xdd(or3 (4, 5, -6))


$\parbox{110mm}{ prints to standard output: \par -{}-{}-{}-{}-{}-{}-{... ...}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-{}-~}$