问题标签 [z3py]

我正在尝试在 上使用ForAll量词，因此每个b公式都会给我结果。我在下面的代码（Z3 python）中实现了这个：a * b == bba == 1

我希望 Z3a = 1在输出时给我，但我得到了Unsat。知道问题出在哪里吗？

（我怀疑我没有正确使用 ForAll，但不知道如何修复它）

示例问题：

假设说谎者总是说假话，说真话的人总是说真话。进一步假设 Amy、Bob、Cal、Dan、Erny 和 Francis 都不是说谎者就是说真话的人。

如果有的话，这些人中有哪些是讲真话的人？

解决方案：

解释：

代码：

输出：

解释：

在此处在线运行此示例

请让我知道您的想法以及是否可以使用 Z3-SMT-LIB 解决此问题。非常感谢。

我将 Z3 与 Python-API 一起使用。我正在设置一组相当大的线性算术约束。

但是，push/pop导致check()无限运行。

如果我不使用任何push/ pop，一切正常。但是当我插入一个

之前的某个地方s.check()，然后s.check()运行无穷无尽。只有使用pushwithout才能pop正常工作。

是否有任何已知的问题和解决方法？我在 MacOS 10.7.5 上使用 Z3 [版本 4.3.1 - 64 位]。

非常感谢和问候，克劳斯

我正在使用 z3py。我的问题是，如何检索Extract节点的边界？我认为Extract这将是一个具有三元数的函数，但它不是：

每个Extract操作（显然）由前两个参数输入（我推断这是因为 decls 不相等）。

如果给我一个BitVecRefwhich 是一个Extract操作，我如何判断操作的范围？因此，对于Extract(i, j, x)我想要一个能够让我返回i和j.

我仍在努力解决寻找a价值的问题，以便a * b == b所有价值都达到b. 预期的结果是a == 1。我有以下两种解决方案。

（A）我ForAll在下面的代码中用量词实现了这个（如果有解决方案而不使用任何量词，请纠正我）。这个想法是证明f和g是等价的。

但是，这个简单的代码会永远运行而不会返回结果。我认为这是因为ForAll. 关于如何解决问题的任何想法？

(B) 我用另一个版本再次尝试。这次我不证明两个公式是等价的，而是把它们都放在一个公式f中。从逻辑上讲，我认为这是真的，但如果我在这里错了，请纠正我：

这次代码没有挂起，而是立即返回“Unsat”。关于如何解决这个问题的任何想法？

非常感谢。

我想使用 z3py 找到给定动作和后置条件的最弱前置条件。

给定动作N = N + 1和后置条件N == 5，最弱的前置条件是 N == 4。

使用战术solve-eqs这种方法适用于某些后置条件，但不适用于其他条件。使用后置条件时，N < 5我得到[[Not(4 <= N)]].

但是当我用N == 5的[[]]时候，我想要的时候N == 4。

这是找到最弱前提条件的最佳方法吗？

我尝试了几种方法，但对 Z3 很陌生，无法弄清楚要采取什么方法或如何实现它。

z3py 表达式的默认输出是中缀表示法。是否可以将输出格式设置为波兰符号？

我认为可能有一个类似于set_option(html_mode=False)但找不到任何支持文档详细说明我可以设置的选项的选项。

目前我正在使用.sexpr()来获取表达式的内部表示。但这在解析时会产生开销，因为它包含我需要过滤的额外信息。

这是我目前正在使用的示例http://rise4fun.com/Z3Py/BNn2

[[N ≤ 4, N ≥ 2]]

我希望它打印为 <= N 4, >= N 2

我可以设置一个选项来更改打印的输出吗？或者是使用.sexpr()表示的最佳方法？

我正在尝试使用以下代码获取无量词公式：

但我正在获得输出：

请你告诉我我的代码会发生什么？非常感谢。

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

我有以下代码可以使用ForAll和Implies执行此操作：

但是，运行上述代码会返回Unsat。我希望这会返回 -4（或 0xfffffffc），所以很困惑。

知道我哪里错了吗？

谢谢！

我无法使用python在z3中执行异或运算。如果我做错了，请帮助告诉我正确的写作方式是什么，否则建议其他一些方式。请尽快回复。