Search

• < Previous
• 1
• Next >

---

Reasoning with Finite Sets and Cardinality Constraints in SMT

Kshitij Bansal ; Clark Barrett ; Andrew Reynolds ; Cesare Tinelli.

We consider the problem of deciding the satisfiability of quantifier-free formulas in the theory of finite sets with cardinality constraints. Sets are a common high-level data structure used in programming; thus, such a theory is useful for modeling program constructs directly. More importantly,&nbsp;[&hellip;]

---

Ground interpolation for the theory of equality

Alexander Fuchs ; Amit Goel ; Jim Grundy ; Sava Krstić ; Cesare Tinelli.

Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence graphs representing derivations in that theory. These graphs&nbsp;[&hellip;]

---