Coypright © 2006 Saarland Univerisity


Caissa implements the eager approach to decision procedures for the quantifier-free theories of equality with uninterpreted symbols, integer linear arithmetic, fixed-size bit-vectors, arrays, sets, multisets, and lists with a length function.

Caissa translates an input quantifier-free formula F into an output CNF propositional formula G such that F is satisfiable modulo the combination of the supported theories if and only if G is propositionally satisfiable.


caissa in [out]

Caissa reads the input formula from the file and writes the output CNF into the file , or into the default file when the second argument is omitted


You can download and use CAISSA under the terms of the following LICENSE.


Questions and bug reports can be emailed to zarba at cs dot uni-sb dot de.