Z3: Is there a way to generate a concrete array that fulfills a Z3 ArrayRef?

I'm trying to get a concrete array fulfilling my Z3 problem. I have the following declaration:

(declare-const MyArray (Array String String))
(assert (= (select MyArray "foo") "bar"))
(assert (= (select MyArray "faz") "bar"))
(check-sat)
(get-model)

Which results in the following Model:

sat
(
  (define-fun MyArray () (Array String String)
    ((as const (Array String String)) "bar"))
)

Is there any way for the model to include the queried indices, like: ["foo"->"bar","faz"->"bar"]?

I tried using Z3Py to see if there was any way to get a better representation of the array but only found an equivalent S-Expression.

Solution

There's no notion of "queried indices" when you write a constraint over an array in SMTLib. Note that this would be a "meta" information: If you want to keep track of which indices were indexed, you should do that yourself in your script. The idea is simple: Instead of calling select you'll call my_select, which will take a look at the index, and keep track of it. And when the time comes to query the model, you can ask for those indexes explicitly. Note that if you call this method with a "symbolic string,", then at the end you'll get the queried value on its model value.

Here's an example:

from z3 import *

keys = []

def my_select(arr, key):
    global keys
    keys += [key]
    return Select(arr, key)

MyArray = Array('MyArray', StringSort(), StringSort())

s = Solver()
s.add(my_select(MyArray, StringVal("foo")) == StringVal("bar"))
s.add(my_select(MyArray, StringVal("faz")) == StringVal("bar"))
s.add(my_select(MyArray, String("symS")) == String("symV"))


r = s.check()
if r == sat:
    m = s.model()
    for key in keys:
        print("MyArray[" + str(m.eval(key)) + "] =",  str(m.eval(Select(MyArray, key))))
else:
    print("Solver said: " + r)

This prints:

MyArray["foo"] = "bar"
MyArray["faz"] = "bar"
MyArray[""] = "bar"

Note, in particular, the last line: The solver internally assigned our symbolic "key" symS the value "", and symbolic value symV, the string value "bar". If you want to avoid getting the symbolic values like this, you should simply not call my_select when you have a symbolic argument.

I'd add that the global keys won't be sufficient if you have multiple arrays (like MyArray1, MyArray2 etc.); in that case you'll have to keep track of a separate list of keys for each array of interest; and figure out a way to distinguish them yourself. But, as I mentioned, this is all "meta"-programming over z3; and really has nothing to do with z3 or SMTLib itself.