** Next:** Reusing functions (Macros)
** Up:** Quick Start - The
** Previous:** An input in canonical
** Contents**

##

An input in XOR format

The XOR format is a specialization of the canonical form allowing
up to two levels of function nesting. However, the grammar of this
format is very different. The following is the
example `.../examples/xortest.xor`:

`p xor 12 3`

`x123 x125 x156 = 0`

`x134 x155x127x167 = 1`

`x1x2x3 x45x145x167 = 0`

which is equivalent to the following canonical form

`p bdd 12 3`

`equ(xor(123, 125, 156), F)`

`equ(xor(134, and(155, 127, 167)), T)`

`equ(xor(and(1, 2, 3), and(45, 145, 167)), F)`

This may be solved using the following command:

`$ sbsat xortest.xor`

The result is shown in Figure .

One peculiarity of this format is that all variables must have names
that begin with `x` and end with a number. No other variable
names are allowed. See Section for important
details concerning this format.

John Franco
2011-09-15