AUFBV logic theory: get value of the array in decimal based format in Z3 model

Question

How to get the value of a variable in Integer sort in QF_AUFBV logic theory?

Consider the following script in SMTLIB2 uses QF_AUFBV logic theory

(set-logic QF_AUFBV)
(set-option :model_compress false)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun out () (Array (_ BitVec 32) (_ BitVec 8) ) )

(assert
(= (concat  (select  out (_ bv3 32) ) (concat  (select  out (_ bv2 32) ) (concat  (select  out (_ bv1 32) ) (select  out (_ bv0 32) ) ) ) )
;; 10<a is false
(ite (=  false (bvslt  (_ bv10 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) )
;;b-15
(bvadd  (_ bv4294967281 32) (concat  (select  b (_ bv3 32) ) (concat  (select  b (_ bv2 32) ) (concat  (select  b (_ bv1 32) ) (select  b (_ bv0 32) ) ) ) ) )
;;b+15
(bvadd  (_ bv15 32) (concat  (select  b (_ bv3 32) ) (concat  (select  b (_ bv2 32) ) (concat  (select  b (_ bv1 32) ) (select  b (_ bv0 32) ) ) ) ) ))))

;;out>15
(assert
(bvsgt (concat  (select  out (_ bv3 32) ) (concat  (select  out (_ bv2 32) ) (concat  (select  out (_ bv1 32) ) (select  out (_ bv0 32) ) ) ) ) (_ bv15 32)))

(check-sat)
(get-model)

When we use Z3 to check the satisfiability it produces the following model.

sat
(model 
  (define-fun b () (Array (_ BitVec 32) (_ BitVec 8))
    (_ as-array k!2))
  (define-fun out () (Array (_ BitVec 32) (_ BitVec 8))
    (_ as-array k!0))
  (define-fun a () (Array (_ BitVec 32) (_ BitVec 8))
    (_ as-array k!1))
  (define-fun k!0 ((x!0 (_ BitVec 32))) (_ BitVec 8)
    (ite (= x!0 #x00000003) #x00
    (ite (= x!0 #x00000002) #x00
    (ite (= x!0 #x00000000) #x11
    (ite (= x!0 #x00000001) #x00
      #x00)))))
  (define-fun k!1 ((x!0 (_ BitVec 32))) (_ BitVec 8)
    (ite (= x!0 #x00000003) #x80
    (ite (= x!0 #x00000002) #x00
    (ite (= x!0 #x00000000) #x0e
    (ite (= x!0 #x00000001) #x00
      #x00)))))
  (define-fun k!2 ((x!0 (_ BitVec 32))) (_ BitVec 8)
    (ite (= x!0 #x00000003) #x00
    (ite (= x!0 #x00000002) #x00
    (ite (= x!0 #x00000000) #x20
    (ite (= x!0 #x00000001) #x00
      #x00)))))
)

Is there any way to print the value of array in decimal-based format? Is it possible to use some C/C++ z3 API to extract the value in decimal-based format? In the given model the value of array out is 17 and b is 32.

Is there any way to avoid (_ as-array k!2))? Just directly print the array value. — user2468460

alias alias · Accepted Answer · 2019-07-31T08:15:46

It's not quite clear what you're asking. But I'm guessing you want to see the values in regular decimal notation as opposed to the default hexadecimal?

If that's the case, then alas there's no direct option to cause the SMTLib output to just use decimals for bit-vectors; as it would be ambiguous from the literal only to figure out how wide it is. However, you can instruct the solver to print the bit-vector values in the so called bv format. Simply call:

z3 pp.bv_literals=false input.smt2

This will print the literals like this:

(_ bv128 8)

The way to read this is that the type is 8-bits wide bit-vector and the value is 128. This is closer to what you're asking, I suppose.

The other option is of course to post-process the output as you see fit; but that goes without saying.

AUFBV logic theory: get value of the array in decimal based format in Z3 model

1 Answers