CODEWITHSUNDEEP
z3
dimo
dimo

Reputation: 53

Why is Z3 having trouble using evenness information under some conditions?

I have the following query that works:

(set-info :status unknown)
(declare-fun n () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= 0 (mod c 2))) ; c is even
(assert (= b (div c 2))) ; b = c/2
(assert (not (= c (* 2 b)))) ; c != 2*b
(check-sat)

As expected I get unsat. However if I substitute c with (n * (n+1)) I get unknown(local z3 built from commit 5068d2083dc0609801f572a0e3d14df753d36a03, roughly 4.5.1) or timeout(on http://rise4fun.com/Z3):

(set-info :status unknown)
(declare-fun n () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= 0 (mod (* n (+ 1 n)) 2)))
(assert (= b (div (* n (+ 1 n)) 2)))
(assert (not (= (* n (+ 1 n)) (* 2 b))))
(check-sat)

Any idea why in one case it figures it out but not in the other?

Thanks! ~Dimo

Upvotes: 1

Views: 41

Answers (1)

alias
alias

Reputation: 30428

When you put in n * (n+1) the problem becomes non-linear. (Non-linear means you multiply/divide by a non-constant.)

In such cases, the default solver is unlikely to produce a result, since the decision algorithms are only for the linear fragment of the logic. You are essentially at the mercy of heuristics: If they can solve your problem, great; if not, you get an unknown for answer.

Having said that, you can use "strategies" to guide the solver. In this case, the following seems to work:

(check-sat-using (and-then qfnra-nlsat smt))

With this, z3 successfully returns unsat for your query.

See http://rise4fun.com/z3/tutorial/strategies for details. It's an art to know what strategy would work for which problem, but if you read through the tutorial you can get a good sense of what to try.

Upvotes: 1

Related Questions