Caissa

[2006-10-16] Coypright © 2006 Saarland Univerisity

Introduction

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.

Usage

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

Download

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

Contact

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