search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Getting unknown with to_real and simple nonlinear arithmetic #2222

Closed jendavis closed 5 years ago

jendavis commented 5 years ago

Here is some observed behavior for a simple nonlinear formula, a*b > 0. I'm using the Z3 tutorial version of Z3 (located at https://rise4fun.com/z3/tutorial) to run these examples.

Over the reals, Z3 determines this is SAT -- no problem.

(declare-const a Real) (declare-const b Real) (assert (> (* a b) 0)) (check-sat)

However, if I start with 'a' as an Int and then convert it to a Real, Z3 returns unknown. Why is this?

(declare-const a Int) (declare-const b Real) (assert (> (* (to_real a) b) 0)) (check-sat)

The above information is enough to understand my question and issue. However, I've included a few other related examples, which also may be useful to the reviewer.

Over the integers, Z3 determines the formula is SAT.

(declare-const a Int) (declare-const b Int) (assert (> (* a b) 0)) (check-sat)

If I start with b as a Real and then convert it to an Int, Z3 determines it is sat--great!

(declare-const a Int) (declare-const b Real) (assert (> (* a (to_int b)) 0)) (check-sat)

If I mix Int and Real without conversion, Z3 returns unknown--this is not a surprise.

(declare-const a Int) (declare-const b Real) (assert (> (* a b) 0)) (check-sat)

Thanks for evaluating this!

NikolajBjorner commented 5 years ago

The current arithmetic solver is highly incomplete for non-linear integer arithmetic. Only formulas that are purely over the reals are solved using a complete stand-alone solver. Note that non-linear integer arithmetic and by extension non-linear mixed integer/real arithmetic is undecidable. The solver makes a best effort attempt. We hope to avoid missing answers to such simple queries as in this example in newer versions of the solver. Hope this helps

jendavis commented 5 years ago

Then perhaps my question is more about how to_real works. I thought that by using to_real, the assertion would be handled the same as it would for reals (in which case Z3 determined the formula was satisfiable). But that's not what happened.

How does to_real work? How is it implemented?

NikolajBjorner commented 5 years ago

to_real is a built-in function. It coerces an integer to real sort. The value of (to_real b) still has to be integral, that is, it has to be -2, -1, 0, 1, 2, … and cannot be 1/2 or 7/8 or sqrt(2). The front-end of Z3 inserts coercions automatically, so if you write ( a b), where a is declared as Real and b as Int, it is parsed as ( a (to_real b)). The SMT-LIB standard includes a definition of to_real, on http://smtlib.cs.uiowa.edu/theories-Reals_Ints.shtml

jendavis commented 5 years ago

OK, that gives me a little more insight at least. And it's good to know that I don't need to even bother with to_real and to_int since they are inserted automatically.