Извлечение Интерполантов Крейга из формулы со строковыми литералами

Question

Я хочу извлечь интерполяции Крейга из формулы, которая также включает строковые литералы.Существуют версии Z3, которые поддерживают извлечение интерполантов, такие как расширение McMillan и SMTInterpol и iZ3, которые поддерживают арифметику и массивы, но ни одна не поддерживает строку.Каков наилучший вариант для формул, которые также имеют строковые операции?

Answer 1

Z3 недавно прекратил поддержку интерполантов, и вряд ли они добавят его обратно в ближайшее время.

MathSAT поддерживает интерполанты, но я не думаю, что он поддерживает строки.

Я не знаюНе думаю, что сейчас есть какой-либо SMT-решатель, который поддерживает как строки, так и интерполяции.