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.
Usagecaissa in [out]
Caissa reads the input formula from the file
Questions and bug reports can be emailed to zarba at cs dot uni-sb dot de.