Geek Answers Handbook

Quantifier Vs Non-Quantifier

I have a question about quantifiers.

Suppose I have an array and I want to calculate the index of the array 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)))

Or else 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 the two of them. The first method is fast and provides a simple and readable model. In contrast, the size of the code with the second option is much smaller, but it takes time to execute the program. And also a difficult decision.

I would like to use the second method, as my code will become smaller. However, I want to find a readable simple model.

+3
source share
1 answer

Justification of a quantifier is usually very expensive. In your example, the quantitative formula is equivalent to the three statements that you have provided. However, this is not how Z3 solves / solves your formula. Z3 solves your formula with a method called Instantiation Quantifier Instantiation (MBQI). This method can solve many fragments (see http://rise4fun.com/Z3/tutorial/guide ). It is mainly effective on the snippets described in this guide. It supports uninterpreted functions, arithmetic and bit-vector theories. It also has limited support for arrays and data types. This is enough to solve your example. The model created by Z3 seems more complicated because the same engine is used to identify more complex fragments. The model should look like a small functional program. You can find more information on how this approach works in the following articles:

Note that array theory is mostly useful for representing / modeling unlimited or large arrays. That is, the actual size of the array is unknown or too large. By large, I mean that the number of calls to the array (i.e. selects ) in your formula is much less than the actual size of the array. We must ask ourselves: "Do we really need arrays to simulate / solve problem X?" You can consider the following options:

  • (Uninterpreted) functions instead of arrays. Your example can also be encoded as:

    (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)))

  • Software API We have seen many examples where arrays (and functions) are used to provide compact coding. Compact and elegant encoding is not always easier to solve. In fact, this is usually the opposite. You can achieve the best of both worlds (performance and compactness) using the software API for Z3. In the following link, I encoded your example using one “variable” for each position of the “array”. Macros / functions are used to encode constraints, such as: expression 0 or 1 . http://rise4fun.com/Z3Py/JF

+3
source

More articles:


All Articles