We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using resolution and quantifier instantiation and computes interpolants (which may contain quantifiers). Arbitrary SMT theories are supported, as long as each theory itself supports tree interpolation for its lemmas. In particular, we show this for the theory combination of equality with uninterpreted functions and linear arithmetic. The interpolants can be tweaked by virtually assigning each literal in the proof to interpolation partitions (colouring the literals) in arbitrary ways. The algorithm is implemented in SMTInterpol.

翻译：我们提出了一种在含量词的SMT（可满足性模理论）背景下通用的树插值算法。该算法利用基于归结与量词实例化的不可满足性证明，计算（可能含量词的）插值项。算法支持任意SMT理论，前提是每个理论自身能对其引理进行树插值。特别地，我们证明了该算法对未解释函数与线性算术联合理论的适用性。通过虚拟地将证明中的每个文字任意分配到插值分区（即对文字着色），可对插值项进行精细调整。该算法已在SMTInterpol中实现。