我有一个关于量词的问题。
假设我有一个数组，我想计算该数组的数组索引 0、1 和 2 -
(declare-const cpuA (Array Int Int))
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1)))
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1)))
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1)))
或者我可以使用 forall 构造指定相同的内容 -
(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1)))))
现在我想了解它们两者之间的区别。
第一种方法执行速度很快，并给出了一个简单易读的模型。
相比之下，第二个选项的代码大小非常小，但程序需要时间来执行。而且解决方案也很复杂。
我想使用第二种方法，因为我的代码会变得更小。
然而，我想找到一个可读的简单模型。
量词推理通常非常昂贵。在您的示例中，量化公式相当于您提供的三个断言。
然而，这不是 Z3 决定/解决你的公式的方式。 Z3 使用称为基于模型的量词实例化 (MBQI) 的技术来求解您的公式。
这种技术可以决定许多片段（参见http://rise4fun.com/Z3/tutorial/guide）。主要对本指南中描述的片段有效。
它支持未解释的函数、算术和位向量理论。它对数组和数据类型的支持也有限。
这足以解决您的示例。 Z3生成的模型看起来更复杂，因为使用相同的引擎来决定更复杂的片段。
该模型应该看起来像一个小型功能程序。您可以在以下文章中找到有关此方法如何工作的更多信息：
量化SMT公式的完整实例化
高效求解量化位向量公式
请注意，数组理论主要用于表示/建模无界数组或大数组。也就是说，数组的实际大小未知或太大。我所说的“大”是指数组访问的数量（即selects）在你的公式中比数组的实际大小小得多。我们应该问自己：“我们真的需要数组来建模/解决问题 X 吗？”。您可以考虑以下替代方案：
-
（未解释的）函数而不是数组。您的示例也可以编码为：
(声明-fun cpuA (Int) Int)
（断言（或（=（cpuA 0）0）（=（cpuA 0）1）））
（断言（或（=（cpuA 1）0）（=（cpuA 1）1）））
（断言（或（=（cpuA 2）0）（=（cpuA 2）1）））
编程式 API。我们已经看到了许多使用数组（和函数）来提供紧凑编码的示例。紧凑而优雅的编码并不一定更容易解决。事实上，通常情况恰恰相反。您可以使用 Z3 的编程 API 实现两全其美（性能和紧凑性）。在下面的链接中，我为“数组”的每个位置使用一个“变量”对您的示例进行了编码。宏/函数用于对约束进行编码，例如：表达式是0 or 1.
http://rise4fun.com/Z3Py/JF
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
