问题标签 [smt]

我们今天遇到了这个看似严重的错误。

考虑这个 Z3 脚本。（为完整起见，转载如下。）

公式是不饱和的。我们首先用一个额外的假设检查公式，并得到unsat预期的结果。然而，当我们再次检查时，没有任何假设，Z3 现在报告sat. 当我们要求一个模型时，我们得到一个明显错误的模型（本质上是矛盾的(distinct 1 1)）。

(check-sat ...)如果我们用(push)和包围第一个(pop)，结果如预期。这表明，当check-sat传递额外的假设时，它会对上下文进行不合理的简化。

我们是否可能check-sat以不正确的方式使用？

有没有推荐的按位向左或向右滚动的方法？

例如带有一个字节 - 0x57 rolr 3 = 0xEA。

我在 Z3py 文档中没有找到任何“滚动”操作。我正在考虑BitVec为每一位使用 s ，但这似乎效率不高/可能行不通。任何建议表示赞赏，谢谢。

编辑：感谢到目前为止的答案。这更像是一个 API 问题，因为我现在很讨厌它。这是我作为起点的内容。

这不会打印任何内容，并且模型不可用。

我需要检查某个 smt 问题的每个令人满意的实例是否有来自其他 smt 问题的匹配实例。即“A 的所有实例都存在 B st ....”的实例，其中 A 和 B 是从一些 smt-lib 代码生成的 sat 模型。

我一直在思考这个问题，但不知道该怎么做

我正在尝试优化使用 Z3 来证明有关一阶理论的事实。目前，我在 Python 中指定了一个一阶理论，将量词固定在那里，并将所有子句连同证明目标的否定一起发送到 Z3。我有以下想法，希望可以优化结果：我只想将与证明目标相关的理论公式发送到 Z3。我不会详细讨论这个概念，但我认为直觉很简单：我的理论是公式的合取，我只想发送可能影响证明目标真值的合取。

我的问题是：这是否会导致效率的提高，或者 Z3 是否已经使用了类似的方法？我猜不会，因为我不认为 Z3 总是假设最后一个断言是证明目标，所以它没有办法对此进行优化。

我有一组 Z3 无法应对的简单约束：

http://pastebin.com/3eaLQ9wx

有没有办法调整约束以获得结果？这是一组更大的约束（数千个）的一个简单示例，但我不知何故感到困扰，即使在这样简单的示例上它也不起作用

提前致谢 ！！

我需要使用 z3 和 mathsat 进行一些实验。我已经完成了 mathsat 的实验。为 mathsat 编写输入文件需要很多时间，我不想再次为 z3 编写输入文件。Mathsat 支持从“msat”文件生成“smt”文件。转换命令如下图：

我的问题是z3可以识别这个'smt'文件吗？

点击查看文件

此文件是否符合 SMT2.0 标准？至少，z3 可以接受它。顺便说一句，“declare-const”和“declare-fun”有什么区别？例如，为了声明一个 Bool 变量，我可以编写declare-const a Boolor declare-fun a() Bool。

我正在使用 Z3 解决由符号执行器产生的路径条件，它以深度优先顺序探索状态空间，与 CUTE、DART 或（可能）SAGE 非常相似。我们正在尝试使用 Z3 的不同方式。在一个极端情况下，我们将每个查询发送到 Z3 并立即（重置）它。另一方面，我们（推）每个额外的分支约束，并且（弹出）（弹出）回溯正确削弱路径条件所需的最小值。问题是，在所有情况下，似乎没有一种策略比其他任何策略都更有效。推送似乎提供了最大的优势，但我们遇到了一些情况，每次查询后重置 Z3 比推送/弹出快一个数量级以上。请注意，通信开销可以忽略不计：几乎所有时间都花在 check-sat 中。

有没有人有任何经验可以分享，或者关于 Z3 内部保存的状态的一些指示（引理等），这可以帮助澄清它的行为？那么其他 SMT 求解器的行为呢？

我想问一下，如何将 Java 与 SMT Z3 求解器集成？如果不仅要描述理论问题，而且还要描述一些实施经验，那就太好了。

我在以下看似微不足道的基准测试中尝试了几个 SMT 求解器（CVC3、CVC4 和 Z3）：

求解器都返回未知数。我知道这是一个无法确定的片段（非线性），但我期待会有一些简单的实例化启发式方法可以解决它。我还尝试使用常量添加一些额外的断言，但它没有帮助。

有没有办法解决这些问题？ SMT 中量化算术的推理限制是什么？