用字符串从公式中提取Craig的插补词

Question

我想从包含字符串文字的公式中提取Craig的插值。有一些版本的Z3支持提取插值，比如McMillan的扩展，以及支持算术和数组但不支持字符串的SMTInterpol和iZ3。对于有字符串操作的公式，什么是最好的选择？

Answer 1

Z3最近放弃了对插值的支持，而且他们不太可能在短期内将其添加回来。

MathSAT支持插值，但我认为它不支持字符串。

我不认为现在有任何支持字符串和插值的SMT求解器。