问题标签 [smt]

因此？

我的问题发生的用例上下文

我定义了一个三角形的 3 个随机项。Microsoft Z3 应输出：

• 约束是否满足或是否有无效的输入值？
• 所有其他三角形项目的模型，其中所有变量都分配给具体值。

为了约束我需要assert三角形等式的项目 - 我想从勾股定理（(h_c² + p² = b²) ^ (h_c² + q² = a²)）开始。

问题

我知道 Microsoft Z3 解决非线性算术问题的能力有限。但即使是一些手动计算器也能够解决这样一个非常简化的版本：

问题

• 如果给出两个值，有没有办法让 Microsoft Z3 解决勾股定理？
• 或者：是否有另一个定理证明器能够处理这些非线性算术的情况？

感谢您对此的帮助 - 如果有任何不清楚的地方，请发表评论。

我在玩未解释的排序和函数，不能完全理解量化公式如何与空模型交互。这里（也在这里http://rise4fun.com/Z3Py/6ets）是一些让我有些困惑的简单例子：

1. [∀v : False]是不饱和的，而“直观地”它适用于空模型。
2. 检查[∃v : v = v]会产生一个空模型，而该模型没有令人满意的分配。
3. 一些看似等同于 的公式以[∃v : v = v]某种方式阻止 z3 生成空模型。[∃v, v1 : v = v1]就是这样一个例子。例如，如果我们将这样的公式添加到求解器，然后尝试创建类似于 allsat 程序的东西（添加越来越多的约束以排除越来越多的模型），我们会在得到一个空模型之前遇到 unsat。

那么，您能否请我参考任何描述 z3 如何处理量词和空模型的文档/论文？另外，如果我选择只关注非空模型，那么询问 z3 的正确方法是什么？诸如此类的事情[∃v, v1 : v = v1]似乎可以解决问题，但是有更好的方法吗？

我想问一下，如何将以下 Z3 约束转换为 Z3py（Python API）。

在下面的工作示例中，我试图检索匹配的模型，在这种情况下有两个令人满意的模型：

和

问题是重复匹配的模型，直到运行求解器超时。如何在不重复的情况下检索满意的模型。

非常感谢，

我有一个简单的提议。我想断言严格排序的整数列表中的第一个元素是列表中所有元素的最小值。我定义排序列表的方式是定义一个局部不变量，即每个元素都小于其下一个元素。我在 Z3 中以以下方式制定了我的主张 -

首先，我想确切地知道哪类公式是有效命题的。我的断言可以归类为有效命题吗？其次，我上面显示的公式是否正确？第三，我应该在 Z3 中设置哪些选项以使其仅在有效命题时才接受量化公式？

我无法让 z3 与 Python 一起工作。我正在运行 Windows 7 64 位。我已经下载了 64 位 Python 3.3.0 和 64 位 z3 4.3.0。我已经更新了我的 PATH 和 PYTHONPATH 以包含 z3 \bin 目录。但是，当我尝试在 python 中使用 z3 时，出现以下错误：

from z3 import * Traceback（最近一次调用最后一次）：文件“”，第 1 行，在 ImportError 中：'z3' 中的坏幻数：b'\x03\xf3\r\n'

有谁知道出了什么问题以及如何解决？

谢谢

我想问一下，如何在 Z3 Python 函数中有超过 255 个参数

在以下工作示例中，如何检索匹配的模型？

例如：作为以下求解器

我正在尝试运行一个非常大的 Z3 python 程序，如以下示例：

我使用了一个集合约束来检索匹配的模型；将根据函数参数检索匹配的模型，如下所示：

但是，我收到以下错误

在 Z3 中使用 SMTLIBv2 输入格式和模式时遇到问题：我不断通过以下输入获得结果“未知”：

我使用一个列表来表示通过转换系统的可能路径。在这种情况下，转换系统仅由状态 L0 和 L1 组成，它们通过从 L0 到 L1 的转换链接。通过断言语句，我将路径限制为以 L0 开头并且长度为 2 的路径。我希望将路径 (L0 (cons (L1 (cons nil)))) 作为模型。

我已经尝试将其归结为一个仍然显示问题的最小示例，从而产生上面的代码。我想使用该模式对“路径”进行递归检查，以确保列表中的每两个连续节点都符合某些（转换）约束。检查连续 cons 用作此递归检查的停止条件。尽管在上面的示例中我通过 checkTransition 删除了递归检查，但它仍然不起作用。整个想法可以追溯到 Milicevic 和 Kugler 的一篇文章，他们使用 Z3 2.0 和 .net API 以这种方式表示模型检查问题。

我知道模式实例化会导致结果“未知”，但我想知道为什么它已经发生在这样一个简单的（？）示例中。我是否以错误的方式使用模式来实现量词支持？

任何关于这个问题的想法都非常受欢迎！

问候卡斯滕

PS：我在 MacOS X (10.8.3) 上使用 Z3 版本 4.3.2 提到的文章：Milicevic, A. & Kugler, H., 2011。使用 SMT 和列表理论进行模型检查。NASA 形式方法，第 282-297 页。

根据 mhs 的评论进行编辑：

4.3.2版本（不稳定）似乎出现了拿不到模型的问题。我对不同版本进行了一些故障排除：

• Z3 4.3.0 32bit，WinXP 32bit，来自安装程序
  • 结果：未知，但给出了一个模型
• Z3版本4.3.1，git checkout 89c1785b73225a1b363c0e485f854613121b70a7，MacOS X，自编译，这是master分支中的最新版本....
  • 结果：未知，但给出了一个模型
• master 分支的各种其他结帐，所有 <= 4.3.1 产生相同的结果。
• Z3 版本 4.3.2，夜间构建 z3-4.3.2.197b2e8ddb91-x64-osx-10.8.2，MacOS X...
  • 结果：未知，给出 NO 模型
• Z3 版本 4.3.2，夜间构建 z3-4.3.2.96f4606a7f2d-x64-osx-10.8.2，MacOS X...
  • 结果：未知，给出 NO 模型

有趣的？