next up previous contents
Next: Prove format Up: Trace format Previous: File Header   Contents

Boolean functions

Boolean functions are specified in the structure section which consists of any number of statements (<statement> in Figure [*]), each terminated by ';'. The keywords STRUCTURE and ENDMODULE must appear by themselves on separate lines. A statement is either


are_equal(<var>, <var>)


which forces both <var>s to have the same value, or


<var> = new_int_leaf([0|1])


which forces <var> to have value F or T if the argument of new_int_leaf is 0 or 1, respectively, or


<var> = <function-identifier>(<var>, ..., <var>)


where <function-identifier> is one of not, and, nand, or, nor, equ, xor, imp, limp, lnimp, rimp, rnimp, ite. The variable lists of all but ite and not can be arbitrarily long. The argument lists for ite and not must have exactly three and exactly one argument(s), respectively. Observe there is no nesting of functions as in the case of the canonical form. Instead, an equality is defined and the leftside (temporary) variable, not appearing in either input or output section, is used as argument in other functions. It is permissable to reference a variable that appears for the first time further ahead in the file. A solution is an assignment to input variables which causes all functions (statements) to have value T.


next up previous contents
Next: Prove format Up: Trace format Previous: File Header   Contents
John Franco 2011-09-15