量词与非量词 [英] Quantifier Vs Non-Quantifier
问题描述
我有一个关于量词的问题.
I have a question about Quantifiers.
假设我有一个数组，我想为这个数组计算数组索引 0、1 和 2 -
Suppose that I have an array and I want to calculate array index 0, 1 and 2 for this array -
(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 构造指定相同的 -
Or otherwise I can specify the same using forall construct as -
(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1)))))
现在我想了解他们两个之间的区别.第一种方法执行速度很快，并提供了一个简单易读的模型.相比之下，第二个选项的代码量很小，但程序需要时间来执行.而且解决方案也很复杂.
Now I would like to understand the difference between two of them. The first method executes quickly and gives a simple and readable model. In contrast the code size with second option is very less, but the program takes time to execute. And also the solution is complex.
我想使用第二种方法，因为我的代码会变小.但是，我想找到一个可读的简单模型.
I would like to use the second method as my code will become smaller. However, I want to find a readable simple model.
推荐答案
量词推理通常非常昂贵.在您的示例中，量化公式等效于您提供的三个断言.但是，这不是 Z3 决定/解决您的公式的方式.Z3 使用一种称为基于模型的量词实例化 (MBQI) 的技术来求解您的公式.这种技术可以决定许多片段(参见 http://rise4fun.com/Z3/tutorial/guide).它主要对本指南中描述的片段有效.它支持未解释的函数、算术和位向量理论.它还对数组和数据类型的支持有限.这足以解决您的示例.Z3 产生的模型看起来更复杂，因为使用相同的引擎来决定更复杂的片段.该模型应该看起来像一个小的功能程序.您可以在以下文章中找到有关此方法如何工作的更多信息:
Quantifier reasoning is usually very expensive. In your example, the quantified formula is equivalent to the three assertions you provided. However, that is not how Z3 decides/solves your formula. Z3 solves your formula using a technique called Model-Based Quantifier Instantiation (MBQI). This technique can decide many fragments (see http://rise4fun.com/Z3/tutorial/guide). It is mainly effective on the fragments described in this guide. It supports uninterpreted functions, arithmetic and bit-vector theories. It also has limited support for arrays and datatypes. This is sufficient for solving your example. The model produced by Z3 seems more complicated because the same engine is used to decide more complicated fragments. The model should be seem as a small functional program. You can find more information on how this approach works in the following articles:
请注意，数组理论主要用于表示/建模无界或大数组.也就是说，数组的实际大小未知或太大.大，我的意思是公式中的数组访问次数(即 selects)比数组的实际大小小得多.我们应该问自己:我们真的需要数组来建模/解决问题 X 吗?".您可以考虑以下替代方案:
Note that, array theory is mainly useful for representing/modeling unbounded or big arrays. That is, the actual size of the array is not known or is too big. By big, I mean the number of array accesses (i.e., selects) in your formula is much smaller than the actual size of the array. We should ask ourselves : "do we really need arrays for modeling/solving problem X?". You may consider the following alternatives:
(未解释的)函数而不是数组.您的示例也可以编码为:
(Uninterpreted) functions instead of arrays. Your example can be encoded also as:
(declare-fun cpuA (Int) Int)
(declare-fun cpuA (Int) Int)
(assert (or (= (cpuA 0) 0) (= (cpuA 0) 1)))
(断言(或(=(cpuA 1)0)(=(cpuA 1)1)))
(断言(或(=(cpuA 2)0)(=(cpuA 2)1)))
(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
这篇关于量词与非量词的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
