CODEWITHSUNDEEP
z3
Wei-Fan Chiang
Wei-Fan Chiang

Reputation: 273

Interpret models returned by QF_FPABV logic

I wrote z3 query in SMT2 format using QF_FPABV logic (quantifier-free floating-point arithmetic and bit-vector logic??). The query is shown as follows: 

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

With 

(check-sat),

I acquired the result and the model as: 

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

This is what I expect. However, if I use 

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

instead, I acquired: 

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

This model is not trivial to interpret...

For this simple example, I can just use (check-sat) to acquire human-readable results. For some complex examples which contains non-linear operations, I need to use (check-sat-using (then simplify solve-eqs bit-blast smt)) to avoid getting "Unknown" from z3...

Is there any document which can teach me to interpret such non-human-readable model?

Upvotes: 4

Views: 248

Answers (2)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The problem here is that the floating-point theory is not fully integrated with the SMT kernel of Z3 yet (I'm working on that in a separate branch). Because of that, the kernel treats all floating-point sorts as uninterpreted and therefore the model contains definitions of those sorts (the universes). At the moment, the best way to get around that is to call the fpa2bv tactic directly, e.g., change

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

to

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

It is necessary to call the simplify tactic before calling fpa2bv and it is also necessary to call the simplifier before the bit-blast tactic, because those tactics rely on the simplifier to eliminate some particular expressions.

Upvotes: 4

alias
alias

Reputation: 30428

I think this is an issue with the model-completion code in Z3. There was a similar bug quite a while ago: Z3 FP logic: produces unexpected model

I thought the issue was already addressed and the code sample in that ticket now works correctly with z3 4.3.2, but apparently the code fragment you presented here triggers a similar problem that's not quite addressed yet.

Upvotes: 1

Related Questions