Z3-str/Z3str2：可以和Z3的其余部分一起使用吗？答案

【问题标题】：Z3-str/Z3str2: can it be used in conjunction with the rest of Z3?Z3-str/Z3str2：可以和Z3的其余部分一起使用吗？
【发布时间】：2016-06-09 08:00:14
【问题描述】：

我们需要一个字符串求解器，并且正在考虑 Z3-str 或其继任者 Z3str2。这些扩展可以同时与 Z3 的所有其余部分（即 Z3 中实现的所有其他理论求解器）一起使用吗？还是这些字符串扩展只能准独立使用？

【问题讨论】：

标签： z3 smt

【解决方案1】：

我不这么认为，不。尝试使用 Z3-str 声明一个实数会出错。似乎只支持字符串和整数。

在使用 Z3-str 之前还有其他事项需要考虑。它似乎需要稍微不同的、不符合 SMT-LIB v2 的输入格式。 Z3-str/tests/ 中提供了示例文件。例如，他们使用declare-variable 来声明变量，而不是declare-const 或declare-fun。

项目中关于 Z3-str 和 Z3-str2 之间的区别也存在一些歧义。具体来说，如果你转到GitHub page，那么在构建说明中会引用Z3-str2.py，但是repo 中没有这样的文件，只有Z3-str.py。我认为 GitHub 页面上的内容仍然是最新版本，因为从 2016 年 2 月开始提交。

最后，Z3-str apparently uses a deprecated API，所以你必须使用旧版本的 Z3。因此，除非您可以使用 Z3 4.1.1（2012 年 10 月），否则您可能不想围绕 Z3-str 构建新项目。

【讨论】：

【解决方案2】：

你很幸运：Z3 目前原生支持字符串。当然，字符串可以与所有其他理论相结合。

【讨论】：