Why do the operators '/' and 'div' in Z3 give different results?
I tried to represent a real number with two integers using them as the numerator and 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 the 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 ab)))' instead of '(assert (= f (/ ab))), then the result is UNSAT. Why doesn't the div return the same result?
Moreover, and the main concern for me I have not found a way to use the '/' operator in the z3.Net API. I only see the MkDiv function, which is actually for the 'div' statement. Is there a way so that I can apply the '/' operator in the case of z3.Net API? Thank you in advance.
source to share
Strictly speaking, none of these formulas meet the SMT-LIB2 requirements 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 creates an Int (see SMT Theories -LIB ). The Z3 is more relaxed and will automatically transform these objects. If we enable the option smtlib2_compliant=true
, then it will indeed report an error in both cases.
The reason there is no invalid version div
is that there is actually no solution where f
is an integer according to (= f (/ a b))
, but there really is no integer that satisfies(= f 0.5)
source to share