Search code examples
z3

Microsoft Z3 solution format understanding

I'm solving SAT problem with Z3. And I get this assignment form Z3:

(model 
(define-fun B ((x!0 Int))
(ite (= x!0 1) false
(ite (= x!0 2) false
  true)))
(define-fun D ((x!0 Int))
 (or (= x!0 3) (= x!0 1))
(define-fun A ((x!0 Int))
  (ite (= x!0 1) false
  (ite (= x!0 4) false
    true)))
(define-fun C ((x!0 Int))
(ite (= x!0 5) false
  true))

I can understand it for B, D, C (B1,B2 are false and others(B3,B4,B5) are true). But how can you meaningfully interpret this OR formula for D? It should be that D1 and D3 are true and D2,D4,D5 are false and it seems it gives right answer. But why it present it in such strange form?

Solution

  • Model printing is not standardized in SMTLib, and depending on what underlying types you use (functions, arrays, scalar types etc.) Z3 will print in some internal format.

    To get individual values, you can always do:

    (eval (D 0))

    etc. to retrieve individual values.