资 源 简 介
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
<
