CODEWITHSUNDEEP
pythonz3z3py
Alberto
Alberto

Reputation: 494

How get an example value from a z3 model for arrays?

Thanks to this question I know how to see the model in an easier way. At this point how can I get the expected values for a and another ?

If possible I'd like the example code using pyz3.

Clarification:

Having the following smt file:

(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and  (=  true (=  (_ bv77 32) (concat  (select  a (_ bv3 32) 
) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) 
(select  a (_ bv0 32) ) ) ) ) ) ) (=  true (=  (_ bv12 32) (concat  
(select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) 
(concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) 
) ) ) ) ) )

I would like to have the value for a and another that are 77 and 12

What is the best way?

At the moment my approach is:

import z3
import binascii

z3.set_param('model_compress', False)
s = z3.Solver()
s.from_file("first.smt")

s.check()

m = s.model()

print(m)


a = m[m.decls()[0]]

print(a)

b = bytearray(a.num_entries())

for x in range(a.num_entries()):
    index = a.entry(x).as_list()[0]
    value = a.entry(x).as_list()[1]

    print(index, value)
    b[a.num_entries()-index.as_long()-1] = value.as_long()

expected = int(binascii.hexlify(b),16)

print(expected)

The output is 77 as expected :)

Thanks

Upvotes: 1

Views: 1769

Answers (2)

alias
alias

Reputation: 30460

The sort of usage you have here is extremely brittle. The line:

a = m[m.decls()[0]]

assumes the model will have the a value in the very first slot. It might work for this particular SMT file; but there's no guarantee that it'll always hold.

Your code can be simplified. But I think that's missing the point that this isn't the proper way to use z3. I'd recommend either sticking to SMTLib only or coding in z3py directly. Mixing those two interfaces is just going to add to confusion for no obvious benefit, and as I mentioned, is going to be extremely brittle.

Since you already seem to have something else generating SMTLib; why not just stick to that format? You can use SMTLib's eval command to extract arbitrary values from your model. Or, recode everythin in z3py, and use those facilities directly. Also, it is not clear why you're modeling a and another as arrays to start with: Seems like you're only interested in the [0]'th element of those arrays? If that's the case, simply use a 32-bit vector instead of an array.

Upvotes: 1

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

As shown in the original question, the model values for arrays are functions that map indices to values. So, an example value for a is [3 -> 1, else -> 1], which is the function that maps index 3 to value 1 and all other indices to value 1.

Upvotes: 1

Related Questions