Search code examples
arraysz3smtz3py

z3py: how to represent an array of integers or characters in z3py

I am new to z3py and SMT and I haven't found a good tutorial about z3py.

Here is my problem setting:

Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5].

I want to infer k for the operator Delete, which deletes the element at position k in an array, where

Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true

Should I use Array or IntVector, or anything else to represent the input/output array?

Edit:

My code is as follows:

from z3 import *

k=Int('k')
s=Solver()

x = Int('x')
y = Int('y')

s.add(k >= 0)
s.add(k < 4)    
s.add(x >= 0)
s.add(x < k)
s.add(y >= k)
s.add(y < 4)

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
Store(I, 0, 1)
Store(I, 1, 2)
Store(I, 2, 3)
Store(I, 3, 4)
Store(I, 4, 5)

Store(O, 0, 1)
Store(O, 1, 2)
Store(O, 2, 4)
Store(O, 3, 5)

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))
print s.check()
print s.model()

It returns 

sat
[I = [2 -> 2, else -> 2],
 O = [2 -> 2, else -> 2],
 y = 1,
 k = 1,
 x = 0,
 elem!0 = 2,
 elem!1 = 2,
 k!4 = [2 -> 2, else -> 2]]

I don't understand what I, O, elem!0, elem!1 and k!4 mean and this is clearly not what I expected.

Solution

  • Disclaimer: I've hardly ever used Z3py before, but I've used Z3 quite a bit.

    I have the feeling that you are somewhat new to encoding logical problems as well - could that be? There are several (odd) things going on in your problem.

    1. You put constraints on x and y, but you actually never use them - instead, you bind different x and y in your quantified assertions. The latter two may have the same names, but they are totally unrelated to the x and y that you constrained (since each forall binds its own variable, you could also use x in both). Hence, your quantified x and y range over all Int, whereas you probably want to limit them to the interval [0..4). Use an implication inside the forall for this.

    2. According to the docs, Store(a, i, v) returns a new array a' that is identical to a, except that x[i] == v. That is, you need to call I = Store(I, 0, 1) etc. in order to finally get an array I that stores your desired values.

    3. Since you don't do this, Z3 is free to pick a model that satisfies your constraints. As you can see from the output, the model for I is [2 -> 2, else -> 2], which says that I[2] == 2, and I[i] == 2 for any i != 2. I don't know why Z3 chose that particular model, but it (together with the model for O) satisfies your foralls.

    4. You can probably ignore elem!0, elem!1 and k!4, they are internally generated symbols.

    5. Here is a reduced version of your example that doesn't verify:

      x = Int('x')  
I = Array('O',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())

I = Store(I, 0, 1)
I = Store(I, 1, 2)

s.add(
  And(
    ForAll(x, Select(O,x) == Select(I,x)),
    ForAll(x, Select(O,x) == Select(I,x+1))))

print s.check() # UNSAT

      The reason why it is unsatisfiable is that I[0] == 1 && I[1] == 2, which contradicts your foralls. If you instantiate both quantified x with 0, the you get O[0] == I[0] && O[0] == I[1] - a constrain that cannot be fulfilled, i.e. there is no model for O that satisfies it.


    Edit (to address a comment):

    If you are puzzled why, given a snippet such as

    I = Array('O',IntSort(),IntSort())
I = Store(I, 0, 1)
I = Store(I, 1, 2)
# print(I)
s.check()
s.model()

    Z3 reports sat and returns a model where I = [], then recall that each Store(...) returns a fresh Z3 expression that represents a store operation, each of which in turn returns a fresh array (which is equal to the initial one, modulo the update). As the print shows, the final value of I is the expression Store(Store(I, 0, 1), 1, 2). It therefore suffices to let I itself be the empty array, i.e. I - the updates (the Stores) will each yield a fresh array (think I1 and I2 in this case), but since they are nameless, they won't (or at least don't have to) show up in the model.

    If you want to explicitly see the "final" values of your array in the model, you can achieve this by giving a name to the array that is created by the last Store, e.g

    I = Array('I',IntSort(),IntSort())
I = Store(I, 0, 1)
I = Store(I, 1, 2)

II = Array('II',IntSort(),IntSort())
s.add(I == II)

s.check()
s.model() # includes II = [1 -> 2, 0 -> 1, else -> 3]