z3 - 量词与非量词

Question

我有一个关于量词的问题。

假设我有一个数组，我想为这个数组计算数组索引 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)))))

现在我想了解他们两个之间的区别。
第一种方法执行速度很快，并提供了一个简单易读的模型。
相比之下，第二个选项的代码量很小，但程序需要时间来执行。而且解决方案也很复杂。

我想使用第二种方法，因为我的代码会变小。
但是，我想找到一个可读的简单模型。

Answer 1

量词推理通常非常昂贵。在您的示例中，量化公式等效于您提供的三个断言。
但是，这不是 Z3 决定/解决您的公式的方式。 Z3 使用一种称为基于模型的量词实例化 (MBQI) 的技术来求解您的公式。
这种技术可以决定许多片段(见 http://rise4fun.com/Z3/tutorial/guide)。它主要对本指南中描述的片段有效。
它支持未解释的函数、算术和位向量理论。它还对数组和数据类型的支持有限。
这足以解决您的示例。 Z3 产生的模型看起来更复杂，因为使用相同的引擎来决定更复杂的片段。
该模型应该看起来像一个小的功能程序。您可以在以下文章中找到有关此方法如何工作的更多信息:

Complete instantiation for quantified SMT formulas

Efficiently Solving Quantified Bit-Vector Formula

请注意，数组理论主要用于表示/建模无界或大数组。也就是说，数组的实际大小未知或太大。大，我的意思是公式中的数组访问次数(即 selects )远小于数组的实际大小。我们应该问自己:“我们真的需要数组来建模/解决问题 X 吗？”。您可以考虑以下替代方案:

(未解释的)函数而不是数组。您的示例也可以编码为:

(declare-fun cpuA (Int) Int)

(assert (or (= (cpuA 0) 0) (= (cpuA 0) 1)))
(assert (or (= (cpuA 1) 0) (= (cpuA 1) 1)))
(assert (or (= (cpuA 2) 0) (= (cpuA 2) 1)))

程序化 API。我们已经看到许多使用数组(和函数)来提供紧凑编码的例子。紧凑而优雅的编码不一定更容易解决。实际上，它通常是相反的。您可以使用 Z3 的编程 API 实现两全其美(性能和紧凑性)。在以下链接中，我为“数组”的每个位置使用一个“变量”对您的示例进行了编码。宏/函数用于编码约束，例如:表达式是 0或 1 .
http://rise4fun.com/Z3Py/JF