next up previous contents
Next: Printing functions Up: Quick Start - The Previous: An input in XOR   Contents

Reusing functions (Macros)

The canonical form only (that is, not cnf or xor formats, among others) supports a rudimentary macro facility. A macro is defined using the directive #define with the following syntax:


#define <pattern> # <function-specifier>


where <pattern> consists of an identifier and a parenthesized argument list. Wherever the <pattern> is matched in the file, <function-specifier> is substituted. Then, <function-specifier> takes as parameters those arguments specified in <pattern>.

Many inputs, particularly those representing an ``unfolding'' of some form of temporal logic, consist of a high percentage of functions which are identical except that all variable input numbers are displaced by some amount. In such a case there is a shortened way to express those functions using #define. For example, the file of Figure [*] may be written equivalently as the file of Figure [*]. More information about #define is found in Section [*], Page [*].

Figure: A canonical form input of ``sliding'' functions.
Figure: An equivalent input using macros.
Figure: Result of executing the command sbsat xortest.xor.
\begin{figure}\begin{verbatim}Reading File xortest.xor ....
Reading XOR ... ...
...)
slide(4, 20, 18, 36, 43)
slide(5, 21, 19, 37, 44)\end{verbatim}
\end{figure}

Figure: A complex canonical form input.
\begin{figure}\begin{verbatim}p bdd 30 11 ; 30 vars, 11 functions
Initial_Bran...
...n created.
; A *' in front of directives is ignored.\end{verbatim}
\end{figure}


next up previous contents
Next: Printing functions Up: Quick Start - The Previous: An input in XOR   Contents
John Franco 2011-09-15