Sciweavers

CADE
2009
Springer

Ground Interpolation for Combined Theories

14 years 4 months ago
Ground Interpolation for Combined Theories
Abstract. We give a method for modular generation of ground interpolants in modern SMT solvers supporting multiple theories. Our method uses a novel algorithm to modify the proof tree obtained from an unsatifiability run of the solver into a proof tree without occurrences of troublesome "uncolorable" literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for convex theories) on the search strategy of the solver. Consequently, it is straightforward to implement and enables more efficient interpolating SMT solvers. In the presence of non-convex theories our method is incomplete, but still more general than previous methods.
Amit Goel, Sava Krstic, Cesare Tinelli
Added 23 Nov 2009
Updated 23 Nov 2009
Type Conference
Year 2009
Where CADE
Authors Amit Goel, Sava Krstic, Cesare Tinelli
Comments (0)