Why operators '/' and 'div' in Z3

问题:

I was trying to represent a real number with two integer numbers as using them as the numerator and the denominator of the real number. I wrote the following program:

(declare-const a Int)
(declare-const b Int)
(declare-const f Real)

(assert (= f (/ a b)))
(assert (= f 0.5))
(assert (> b 2))
(assert (> b a))

(check-sat)
(get-model)

The program returned SAT result as follows:

sat
(model 
  (define-fun f () Real
    (/ 1.0 2.0))
  (define-fun b () Int
    4)
  (define-fun a () Int
    2)
)

However, if I write '(assert (= f (div a b)))' instead of '(assert (= f (/ a b)))', then the result is UNSAT. Why does not div return the same result?

Moreover, and the main concern for me, I did not find a way to use operator '/' in z3 .Net API. I can see only function MkDiv, which actually for operator 'div'. Is there a way so that I can apply operator '/' in the case of z3 .Net API? Thank you in advance.

回答1:

Strictly speaking neither of these formulas is SMT-LIB2 compliant, because / is a function that takes two Real inputs and produces a Real output, whereas div is a function that takes two Int inputs and produces an Int (see SMT-LIB Theories). Z3 is more relaxed and automatically converts those objects. If we enable the option smtlib2_compliant=true then it will indeed report an error in both cases.

The reason for the div version being unsatisfiable is that there is indeed no solution where f is an integer according to (= f (/ a b)), but there is indeed no integer that satisfies (= f 0.5)