CSIsat is an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementation combines the efficiency of linear programming for solving the arithmetic part with the efficiency of a SAT solver to reason about the boolean structure.

CSIsat Project Home Page

• Please visit the CSIsat Project Home Page

Documentation

• Tool paper at CAV 2008: CSIsat: A Tool for LA+EUF Interpolation Proc. CAV'08, LNCS 5123, pages 304-308, Springer-Verlag, 2008.
• API and source code documentation
• Tutorial coming soon.
• Quick reference

Downloads

• The download list provides archived source code and binaries for released versions
• Check out the latest version
• To build from source code, read the installation instructions

Problem Reports

• Mail to: Dirk Beyer (first.last@sfu.ca) or Damien Zufferey (first.last@epfl.ch)

Acknowledgements

• We thank many other people for their contributions.