问题标签 [z3py]

我写了上面的代码，但它不起作用。它没有将字符串作为输入，我无法找到它接受的输入类型。

给定c == a + 4和t == c + b，如果b == -4，那么t == a。我试图做相反的事情，这意味着给定上述 2 个等式和t == a，我试图找到 的值b。

这与相关问题非常相似，但这次我只切换aand b，我真的很困惑代码返回不同的结果。

按照上面链接中发布的代码，我有以下代码（类似，仅a和b切换）：

但是，在 Ubuntu 上，运行上述代码会返回意外结果Unsat，但不会返回值-4（或0xfffffffc）

知道为什么这是错误的吗？

非常感谢。

我正在使用 Z3 检查数组属性片段中公式的可满足性。Z3 返回的数组变量模型通常使用其他 if 表达式、if-then-else 案例分析等来表示。我想以某种方式解析 Z3 输出的模型并创建满足输入 SMT-LIB 公式的数组，明确的。

例如，我希望能够以某种方式始终将 Z3 输出的模型简化为以下形式：

是否有一些简单的方法来遍历模型（使用 C API？）并创建一个表示模型的显式数组？

我正在使用以下代码：

输出为：在此处在线运行此示例

在此示例中，矩阵 M 将 2-SAT 实例定义为 CNF（参考）。在这个例子中，矩阵 M 是手动引入的。请让我知道如何自动引入矩阵 M ( matrix )。非常感谢。

TL;DR：使用 时，位向量划分节点从Z3_OP_BSDIV变为。如何从未解释的操作中分辨出除法操作？Z3_OP_UNINTERPRETEDsimplify

解释：

以下会话显示位向量除法被解释，但在使用 之后simplify()，它是未解释的。看看d下面的变量会发生什么。

我们可以看到手动声明的未解释函数也UDiv具有相同的类型。

但是，它似乎并不影响求解：求解器似乎仍将运算解释为实际除法。

我正在尝试按它们的种类处理节点，但是这个似乎“撒谎”了它的种类——有没有办法知道它真的被解释了，即使它kind是Z3_OP_UNINTERPRETED？这是一个错误吗？

请考虑以下 3-SAT 实例和相应的图表

图表可以用其他两种形式显示

该图的 Tutte 多项式为

图的独立数为 4，则考虑的 3-SAT 实例是可满足的。使用以下代码检查这一事实：

相应的输出是：

图的对应补码是

并且图的补码的 Tutte 多项式是

补集的团数是 4，然后它表示所考虑的 3-SAT 实例是可满足的。

问题是：是否可以使用 Tutte 多项式来确定所考虑的 3-SAT 实例是否可满足？

在 Z3Py 中，是否可以获得出现某些变量/表达式的所有公式的列表？一个例子：

I am trying to simplify an expression using z3py but am unable to find any documentation on what different tactics do. The best resource I have found is a stack overflow question that lists all the tactics by name.

Is someone able to link me to detailed documentation on the tactics available? The on line python tutorials are not sufficient.

Or can someone recommend a better way to accomplish this.

An example of the problems is an expression such as:

x < 5, x < 4, x < 3, x = 1 I would like this to simplify down to x = 1.

Using the tactic unit-subsume-simplify appears works for this example.

But when I try a more complicated example such as x > 1, x < 5, x != 3, x != 4 I get x > 1, x < 5, x ≠ 3, x ≠ 4 as the result. When I would like x = 2.

What is the best approach to achieve this type of simplification using z3py?

My current solution.

Thanks Matt

多年来，我一直在跟踪解决技术问题——并且我维护了一篇关于将它们应用于特定难题的博客文章——“交叉梯子”。

言归正传，我无意中发现了 z3，并尝试将其用于具体问题。我使用了 Python 绑定，并写了这个：

不幸的是，z3 报告...

这个问题至少有这个整数解：a=34, b=50, c=42, d=105, e=16, f=40。

我做错了什么，还是这种方程组/范围约束超出了 z3 可以解决的范围？

提前感谢您的帮助。

更新，5 年后：Z3 现在开箱即用地解决了这个问题。

我是 Z3 的新手，我正在查看在线 python 教程。

然后我想我可以检查 BitVecs 中的溢出行为。

我写了这段代码：

我期待 [y = 7, x = 7] （即当值相等但后继者不相等时，因为 x + 1 将是 0 而 y + 1 将是 8）

但是 Z3 回答 [y = 0, x = 0]。

我究竟做错了什么？