z3 - 解释 QF_FPABV 逻辑返回的模型

Question

我使用 QF_FPABV 逻辑(无量词浮点运算和位向量逻辑？？)以 SMT2 格式编写了 z3 查询。
查询如下所示:

(set-logic QF_FPABV)
(set-option :produce-models true)

(declare-fun f0 () (_ FP 8 24))
(declare-fun f1 () (_ FP 8 24))
(declare-fun f2 () (_ FP 8 24))

(assert (= f2 (* roundNearestTiesToEven f0 f1)))
(assert (>= f2 ((_ asFloat 8 24) roundNearestTiesToEven 3.0 0)))

(check-sat)
; (check-sat-using (then simplify solve-eqs bit-blast smt))
(get-model)

和

(check-sat), 

我获得的结果和模型为:

sat                                                                             
(model                                                                          
  (define-fun f2 () (_ FP 8 24)                                                 
    (as +1.44919359683990478515625p127 (_ FP 8 24)))                            
  (define-fun f1 () (_ FP 8 24)                                                 
    (as +1.476345062255859375p0 (_ FP 8 24)))                                   
  (define-fun f0 () (_ FP 8 24)                                                 
    (as +1.9632179737091064453125p126 (_ FP 8 24)))                             
)

这是我所期望的。
但是，如果我使用

(check-sat-using (then simplify solve-eqs bit-blast smt)) 

相反，我获得了:

sat
(model
  ;; universe for RoundingMode:
  ;;   RoundingMode!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun RoundingMode!val!0 () RoundingMode)
  ;; cardinality constraint:
  (forall ((x RoundingMode)) (= x RoundingMode!val!0))
  ;; -----------
  ;; universe for (_ FP 8 24):
  ;;   FP!val!0 FP!val!1 FP!val!2 FP!val!3
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun FP!val!0 () (_ FP 8 24))
  (declare-fun FP!val!1 () (_ FP 8 24))
  (declare-fun FP!val!2 () (_ FP 8 24))
  (declare-fun FP!val!3 () (_ FP 8 24))
  ;; cardinality constraint:
  (forall ((x (_ FP 8 24)))
          (or (= x FP!val!0) (= x FP!val!1) (= x FP!val!2) (= x FP!val!3)))
  ;; -----------
  (define-fun f1 () (_ FP 8 24)
    FP!val!2)
  (define-fun f0 () (_ FP 8 24)
    FP!val!1)
  (define-fun f2 () (_ FP 8 24)
    (* roundNearestTiesToEven FP!val!1 FP!val!2))
)

这个模型并不容易解释......

对于这个简单的例子，我可以使用 (check-sat) 来获取人类可读的结果。
对于一些包含非线性操作的复杂示例，
我需要使用(check-sat-using(然后简化solve-eqs bit-blast smt))
避免从 z3 获得“未知”...

有什么文件可以教我解释这种非人类可读的模型吗？

Answer 1

这里的问题是浮点理论还没有与 Z3 的 SMT 内核完全集成(我正在一个单独的分支中研究它)。因此，内核将所有浮点排序视为未解释的，因此模型包含这些类型(宇宙)的定义。目前，解决这个问题的最好方法是直接调用 fpa2bv 策略，例如，更改

(check-sat-using (then simplify solve-eqs bit-blast smt)) 

到

(check-sat-using (then simplify fpa2bv simplify solve-eqs bit-blast smt)) 

在调用 fpa2bv 之前需要调用简化策略，并且在 bit-blast 策略之前调用简化策略也是必要的，因为这些策略依赖于简化来消除某些特定的表达式。