next up previous contents
Next: File Header Up: Reference - Input formats Previous: Prove format   Contents

SMURF format

This input format is intended for low-level truth table input. Variables are represented as positive integers. Any set of Boolean functions can be accomodated. Each function is specified in a section of three lines: the first line numbers the function, the second line specifies the variables that the function depends on, the third line specifies the truth table of the function or uses function symbols to denote commonly used functions. All function sections are separated by a hash ('#') character, which is itself on a separate line. A list of functions is terminated with the character '@' on a line by itself at the end of the file. The header contains a line indicating a goal value for each function. A solution to the problem defined in a file is an assignment causing all Boolean functions to attain their goal value. There are no comments, manipulators, or directives in this format.


John Franco 2011-09-15