5

I'm experimenting with z3 in python. I have the following model:

(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  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) (concat  (select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) (concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) ) ) ) ) ) )

I can load it and check that is sat. At this point how can I get an example value for a and another?

import z3
s = z3.Solver()
s.from_file("first.smt")
"""
s
[And(False ==
     (77 == Concat(a[3], Concat(a[2], Concat(a[1], a[0])))),
     False ==
     (12 ==
      Concat(another[3],
             Concat(another[2],
                    Concat(another[1], another[0])))))]
"""
s.check()
"""
sat
"""
m = s.model()
m
[a = Lambda(k!0, 1), another = Lambda(k!0, 1)]

Thanks

Alberto
  • 446
  • 5
  • 14

1 Answers1

2

Z3 produces Lambda abstractions for arrays by default; which are useful but hard to see what's going on in a model. I'd recommend turning that off, by putting the following line in your python program:

z3.set_param('model_compress', False)

You should do this right after you import z3.

With this, if you print the model in your program, you get:

>>> m
[a = [3 -> 1, else -> 1],
 another = [1 -> 1, else -> 1],
 k!0 = [3 -> 1, else -> 1],
 k!1 = [1 -> 1, else -> 1]]

which should be more readable. (It's essentially saying both a and another are arrays that map everything to 1; though a bit convoluted.)

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks for your answer, I was able to have the model in that format now. I'd ask you another clarification if possible. I edited my original question for that. Could you explain more in details the model. Thanks – Alberto Nov 12 '18 at 18:30
  • 1
    On stack-overflow, it's always best to start a different question instead of editing the original. Also, "accepting" the answer tells others the issue is resolved; both for people having similar issues and the people trying to help others out. Comments should be reserved only for the original discussion. So, please start a new question and I'm sure someone will answer! – alias Nov 12 '18 at 18:34