Overview
--------

This is a simple boolean calculator.  It reads a boolean formula and checks
whether it is valid.  In case '-s' is specified satisfiability is checked
instead of validity.

Language
--------

The input format has the following syntax in BNF:
( [ ... ] means optional,  { ... } means repeated arbitrary many times)
   
   expr ::= iff
   iff ::= implies { '<->' implies }
   implies ::= or [ '->' or ]
   or ::= and { '|' and }
   and ::= not { '&' not }
   not ::= basic | '!' not
   basic ::= var | '(' expr ')'

and 'var' is a string over letters, digits and the following characters:
  
  - _ . [ ] $ @

The last character of 'var' should be different from '-'.

Install
-------

Please get the 'limmat' SAT solver (version >= 1.2) and unpack it in the
same directory where you have unpacked 'limboole'.  Before you compile
'limboole' you have to generate 'liblimmat.a' in the 'limmat' subdirectory.
Then change to the 'limboole' subdirectory and issue 'make' to compile it.
This should also generate the test suite 'testlimboole'.  Run it to check
that everything works.

To check coverage of the test cases you have to instrument the code for
profiling by changing the order of the lines defining CFLAGS in the
Makefile.   Then compile 'testlimboole' as usual and run the testsuite.
Afterwards 'gcov limboole.c' will give you coverage information.

There is also a small utility 'dimacs2boole' that can be used to translate
CNF formulae in DIMACS format to the input format of 'limboole'.

Armin Biere, Computer Systems Institute, ETH Zurich
Wed May 14 13:25:49 CEST 2003