解释 QF_FPABV 逻辑返回的模型答案

【问题标题】：Interpret models returned by QF_FPABV logic解释 QF_FPABV 逻辑返回的模型
【发布时间】：2014-05-23 17:31:53
【问题描述】：

我使用 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 获得“未知”...

是否有任何文件可以教我解释这种非人类可读的模型？

【问题讨论】：

标签： z3

【解决方案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之前需要调用simplifier策略，在bit-blast策略之前调用simplifier也是必要的，因为这些策略依赖simplifier来消除一些特定的表达式。

【讨论】：

【解决方案2】：

我认为这是 Z3 中模型完成代码的问题。很久以前有一个类似的错误：Z3 FP logic: produces unexpected model

我认为该问题已得到解决，并且该票证中的代码示例现在可以在 z3 4.3.2 中正常工作，但显然您在此处提供的代码片段触发了一个尚未完全解决的类似问题。

【讨论】：