我遇到了一个问题，在一个更大的系统中嵌入的z3代码没有找到解决某组约束(通过C++接口添加)的方法，尽管超时时间相当长。当我将约束转储到一个文件中(使用求解器上的to_smt2()方法，就在调用check()之前)，并通过独立的z3可执行文件运行该文件时，它在大约4秒内解决了系统(返回sat)。就其价值而言，该文件有476587行长，因此有一组相当大的约束。
有没有一种方法可以使用C++接口将该文件读取回嵌入式解算器，替换现有的约束，看看嵌入式版本是否可以从与独立解算器完全相同的起点开始求解？(本质上，我如何在求解器类上创建相应的from_smt2(流)方法？)
当然，它们应该是与现在相同的一组约束，但当从文件中读取它们时，可能会产生一些排序效应，或者当我们嵌入它时，在求解器中引入了一些细微的差异，或者没有用to_smt2()写出一些东西。因此，如果可以的话，我想试着读回文件，以缩小差异的可能来源。关于调试长时间运行的版本时要查找什么的建议也很有帮助。
进一步注意：看起来另一个用户也有类似的问题。与那个用户不同，我的问题使用了所有的位向量，唯一未知的结果是来自嵌入代码的结果。有没有一种方法可以从C++接口调用(get-info：原因未知)，就像那里建议的那样，找出嵌入式版本出现问题的原因？
您可以使用方法"solver：：reason_nunknown()"来检索搜索失败的解释。有一些方法可以将文件和字符串解析为单个表达式。在一组断言的情况下，表达式是一个连词。为了方便起见，将这样的方法直接添加到求解器类中可能是个好主意。应该是：
void from_smt2_string(char const* smt2benchmark) {
expr fml = ctx().parse_string(smt2benchmark);
add(fml);
}
因此，如果你要在求解器类之外编写它，你需要：
expr fml = solver.ctx().parse_string(smt2benchmark);
solver.add(fml);