AUFBV逻辑理论:在Z3模型中以基于十进制的格式获取数组的值

Question

如何在qf_aufbv逻辑理论中以整数排序中的变量的值？

考虑smtlib2中的以下脚本使用qf_aufbv逻辑理论

(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)

当我们使用Z3检查可满足性时，它会产生以下模型。

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)))))
)

有什么方法可以以十进制格式打印数组的值？是否可以使用一些C/C Z3 API以基于小数的格式提取值？在给定模型中，数组的值为17，b为32。

Answer 1

尚不清楚您要问什么。但是我猜您想以常规十进制符号而不是默认的十六进制来查看这些值？

如果是这种情况，则没有直接的选择使Smtlib输出仅对位矢量使用小数。从字面上看，这是模棱两可的，只是弄清楚它的宽度。但是，您可以指示求解器以所谓的 bv 格式打印比特矢量值。只需致电：

z3 pp.bv_literals=false input.smt2

这将打印出这样的文字：

(_ bv128 8)

阅读此书的方法是类型是8位宽的位矢量，值为128。我想这更接近您的要求。

另一种选择当然是在您认为合适的情况下进行后处理；但这不用说。