Instantiation-Based Interpolation for Quantified Formulae in CSIsat
Vadim Mutilin, Mikhail Usamovich Mandrykin · Proceedings of the Spring/Summer young researchers' colloquium on software engineering · 2012
The paper describes an implementation of instantiation-based interpolation for quantified formulae in modified CSIsat tool.The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers.We propose in this paper using external SMT-solver CVC3 for quantified expressions instantiation, then we describe how we modified CSIsat and CVC3 tools in order to support quantified formulae interpolation.We also present results of benchmarking the modified CSIsat tool on SMTLIB test set as well as on our specially generated interpolation tasks.