Why does 0 = 0.5?

Question

I noticed some strange behavior with Z3 4.3.1 when working with .smt2 files.

If I do (assert (= 0 0.5)) it will be satisfiable. However, if I switch the order and do (assert (= 0.5 0)) it's not satisfiable.

My guess as to what is happening is that if the first parameter is an integer, it casts both of them to integers (rounding 0.5 down to 0), then does the comparison. If I change "0" to "0.0" it works as expected. This is in contrast to most programming languages I've worked with where if either of the parameters is a floating-point number, they are both cast to floating-point numbers and compared. Is this really the expected behavior in Z3?

Answer 1

I think this is a consequence of lack of type-checking; z3 is being too lenient. It should simply reject such queries as they are simply not well formed.

According to the SMT-Lib standard, v2 (http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf); page 30; the core theory is defined thusly:

(theory Core
:sorts ((Bool 0))
:funs ((true Bool) (false Bool) (not Bool Bool)
      (=> Bool Bool Bool :right-assoc) (and Bool Bool Bool :left-assoc)
      (or Bool Bool Bool :left-assoc) (xor Bool Bool Bool :left-assoc)
      (par (A) (= A A Bool :chainable))
      (par (A) (distinct A A Bool :pairwise))
      (par (A) (ite Bool A A A))
      )
:definition
"For every expanded signature Sigma, the instance of Core with that signature
is the theory consisting of all Sigma-models in which:
  - the sort Bool denotes the set {true, false} of Boolean values;
  - for all sorts s in Sigma,
       - (= s s Bool) denotes the function that
         returns true iff its two arguments are identical;
       - (distinct s s Bool) denotes the function that
         returns true iff its two arguments are not identical;
       - (ite Bool s s) denotes the function that
         returns its second argument or its third depending on whether
         its first argument is true or not;
       - the other function symbols of Core denote the standard Boolean operators
         as expected.
       "
  :values "The set of values for the sort Bool is {true, false}."
)

So, by definition equality requires the input sorts to be the same; and hence the aforementioned query should be rejected as invalid.

There might be a switch to z3 or some other setting that forces more strict type-checking than it does by default; but I would've expected this case to be caught even with the most relaxed of the implementations.

Answer 2

Do not rely on the implicit type conversion of any solver. Instead, use to_real and to_int to do explicit type conversions. Only send well-typed formulas to the solver. Then Mohamed Iguernelala's examples become the following.

(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= (to_real x) 1.5))
(check-sat)
(exit)

(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= 1.5 (to_real x)))
(check-sat)
(exit)

Both of these return UNSAT in Z3 and CVC4. If instead, you really wanted to find the model where x = 1 you should have instead used one of the following.

(set-option :produce-models true)
(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= (to_int 1.5) x))
(check-sat)
(get-model)
(exit)

(set-option :produce-models true)
(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= x (to_int 1.5)))
(check-sat)
(get-model)
(exit)

Both of these return SAT with x = 1 in Z3 and CVC4.

Once you make all the type conversions explicit and deal only in well-typed formulas, the order of arguments to equality no longer matters (for correctness).