问题标签 [z3py]

是否可以在 Z3 中禁用布尔表达式的自动简化？

例如，表达式 2 > 1 自动变为 True，而我希望它保持 2 > 1：

我通过在 Z3Py 中调用 help_simplify() 找到了几个选项。但是，它们似乎都与我的问题无关。

在另一个教程（http://citeseerx.ist.psu.edu/viewdoc/download?rep=rep1&type=pdf&doi=10.1.1.225.8231）中提到了一个选项“CONTEXT SIMPLIFIER”：“此设置可用于简化子-公式判断真假。” 但是，我在 Z3Py 中找不到这个选项。

背景：我希望能够使用像 And(2>1, 1!=2) 这样的表达式，其中 2>1 和 1!=2 是较早自动生成的，有时不包含变量（常量）。Z3Py 将其简化为不被接受的 And(True, False)，因为“至少有一个参数必须是 Z3 表达式或探针”。因此，我想抑制简化。或者有没有办法让 And(True, False) 成为可接受的表达式？

提前致谢！

有人可以帮助了解如何在 Z3 中正确使用“for all”吗？我一直在查看文档，但找不到信息。我想做的是

在“foo”中，我需要在 Z3 中说一些相当于

“让（u，r）在{（断言（（u，r）在用户中）（断言（r，t）在角色中）}中可运行（t）”

我不知道如何将 runnable 中的第一个元素断言在用户中，然后将第二个元素断言在角色中。

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) ) 布尔)

(assert (forall (t Task)) (foo))

(check-sat) (get-model)

据我所知，我可以声明一个返回多个元素的函数。假设我有一个函数 x，它接收一个排序 T 并返回一个排序 U 和一个排序 R

(declare-sort T) (declare-sort R) (declare-sort U)

（声明乐趣 x (T) (UR)）

那么，当调用函数 x 返回元素时，我该如何访问......可以说我需要断言将 U 传递给一个函数，将 R 传递给另一个函数.. 可以这样做吗？

我正在尝试通过其 Python 接口使用 Z3 来推断简单线性公式的可满足性。即使在我以 smt2 格式写下的以下简单公式（由 10 个子句和每个 10 个术语组成）之类的简单公式上，它似乎也很慢：

我正在使用以下代码块动态生成这些公式：（注意：公式是子句列表；子句是术语列表、比较符号和自由系数；术语是一对变量标识符（整数)，变量的系数（整数））。

我遇到的问题是 Z3 被困在这样的公式上。当我将它保存到名为 formula.smt2 的文件并尝试通过 bash Z3 命令解决它时，它似乎也被卡住了。

我使用的求解器版本是：Z3 version 4.3.2

是我使用的格式不方便还是因为 Z3？有什么技巧可以用来加快求解过程吗？

正如胡安·奥斯皮纳建议的那样，我试图找出公式的哪一部分对求解器来说是困难的。它似乎是以下内容：

事实上，如果你从这个公式中删除任何子句，求解器能够在不到一秒钟的时间内回答，而如果你用整个公式来输入它，它就会超时。

为什么会这样？Z3觉得这个公式这么难解是正常的吗？

最好的，安德里亚

我试图影响 Z3 生成的模型值结果的随机性。据我了解，对此的选择非常有限：在线性算术的情况下，单纯形求解器不允许仍然满足给定约束的随机结果。但是，有一个选项 smt.arith.random_initial_value （“在基于单纯形的过程中使用随机初始值进行线性算术（默认值：false）”）我似乎无法正常工作：

结果，这似乎总是产生 [y = 0, x = 1]。即使是在给定约束中未使用的变量的模型完成似乎总是会产生确定性的结果。

关于此选项如何工作的任何想法或提示？

我尝试使用位向量在模型值中获得随机结果，例如 de Moura 建议的模型值，但随后使用 Z3Py 而不是 SMTLIB。我把他的例子翻译成：

但是，结果似乎总是相同的，即 - 使用 s.check() 重复检查不会改变结果。- 即使在 python 交互式 shell 重新启动后，执行的结果也是一样的

添加随机种子的更改不会改变结果： set_option('smt.random_seed', 123)

有谁知道为什么不能按预期工作？

提前致谢！

卡斯滕

我想找到一个纯 python z3 包，它可以帮助我在谷歌应用引擎中运行 z3。我在本地运行了以下 python 测试并运行：

但它需要这些文件才能使其工作：z3.pyc、z3consts.pyc、z3core.pyc、z3printer.pyc、z3types.pyc、libz3.dylib。我通过从 z3 codeplex 站点下载构建 z3 来获得这些文件。

因此，将这些文件放在我的 app id 文件夹内的“lib”文件夹中，我尝试了以下 main.py 的改编（谷歌提供的“hello world”程序）：

在应用程序引擎启动器中运行的这段代码为我提供了一个空白页并且没有错误消息。

如果我注释掉所有与 z3 相关的代码，我会收到一条 hello world 消息，正如预期的那样。

注意：我已经阅读了关于如何包含 3rd 方库的文章 14850853，并已使用 BeautifulSoup 成功对其进行了测试。我的问题是关于纯 python z3 库的可用性。

从谷歌关于沙盒的文档中，我很确定 *.pyc 文件没问题，但我认为这些文件需要工作的 (16MB) libz3.dylib 不是纯 python。是否存在 z3 的纯 python 版本，或者是否有其他方法可以在我错过的应用引擎上使用 z3？

我正在使用 python 和 z3py 模块编写一些程序。
我要做的是以下内容：我从位于其他文件中的函数中提取 if 或 while 语句的约束。此外，我提取语句中使用的变量及其类型。
由于我不想手动将约束解析为 z3py 友好的形式，因此我尝试使用评估来为我执行此操作。因此我使用了以下页面的提示：Z3 with string expressions
现在问题是：我不知道约束中的变量是如何调用的。但似乎我必须将每个变量的句柄命名为实际变量。否则评估不会找到它。我的代码如下所示：

如您所见，我将变量和约束保存在类中。执行此代码时，我收到以下错误：

如果我不使用对变量的循环，而是使用以下代码，则一切正常：

问题是：我不知道这些变量被称为“real_x”还是“int_y”。此外，我不知道使用了多少变量，这意味着我必须使用一些动态的东西，比如循环。

现在我的问题是：有没有办法解决这个问题？我该怎么做才能告诉 python 句柄已经存在，但名称不同？还是我的方法完全错误，我必须做一些完全不同的事情？

我正在使用来自 Codeplex 的最新 z3 主代码，标记为 v4.3.1。

我想要一个这样的函数prove，它有一个有用的返回值并且不打印。所以，我写了看起来很明显的东西：

但是，此代码的运行速度比默认prove函数慢得多。

prove（瘦身）的代码src/api/python/z3.py是：

当我添加s.set()到我的代码中时，它很快并且找到了相同的反例。

这里发生了什么？

• 这个空洞的电话是否以s.set()某种方式清除了一些通常不好的选项？
• ..对我的特定测试不利？
• 还有什么？

我试图找出默认的求解器选项是什么，但是str(s) repr(s),s.__dict__和 google 并没有真正帮助。

任何建议表示赞赏！

我正在尝试使用 java API 学习 Z3，因为没有文档我一直在查看 C API 文档，但直到现在我找不到一个清楚的例子来说明如何使用一些基本功能。

我正在尝试编码这个 Z3 代码（在在线版本中有效）

到目前为止，我只是设法声明未解释的排序并声明我的函数如下

但我找不到一个例子来表达

有人可以帮我解决这个问题吗？用 java API 表达这个断言的方法是什么？