【发布时间】：2019-08-29 06:06:43
【问题描述】：
考虑以下在 Klee 的帮助下生成的smt2 file。
我正在尝试使用 z3 对其进行评估。但是，z3 永远挂起。具体来说，当公式为 UNSAT 时，z3 将永远运行并且不会产生任何结果。
- 公式大小大吗？
- 使用逻辑理论AUBFV时有什么问题吗？
我可以得到一些建议来提高 z3 的性能。
每个断言语句都有一些公共子表达式。是否可以通过单独求解子表达式来提高z3的性能？
【问题讨论】：
【发布时间】：2019-08-29 06:06:43
【问题描述】：
这将无法回答，因为您链接的 SMT-lib 文件对于非 KLEE 用户来说是无法破译的。我建议直接使用导致此问题的原始程序询问 KLEE 人员。如果做不到这一点，请尝试将 SMT2Lib 减少到最低限度，看看您是否至少可以手动注释以查看它正在尝试做什么。
关于常见子表达式的问题：您必须进行实验才能找到答案。但是大多数此类求解器的构造方式是，它们/将/自己发现公共子表达式并在将您的输入转换为内部表示时自动重用关于它们的引理。因此，如果它以任何显着的方式帮助手动完成这项工作，我会感到惊讶。除非输入真的很大。 （您链接的示例并没有那么大，所以我怀疑这是一个问题。）
【讨论】：
-
Klee 没有问题。我不知道如果我将此文件作为输入提供给 z3，那么它会失败并永远存在。请注意，公式未饱和，但 z3 挂起。如果我修改一些条件使其成为 sat，那么 z3 也会报告 sat 并生成一个模型。
-
也许可以试试其他求解器？ CVC4、MathSAT、Yices？他们中的任何一个设法解决它吗？这可能太难证明了。