2

This is the reduction of a more interesting problem, in which the missing property was (for positive k,M and N), that ((k % M) * N) < M*N. Below is an encoding of the simpler problem that a <= b ==> (a*c) <= (b*c). Such a query succeeds (we get unsat), but if the expression b is replaced by b+1 (as in the second query below) then we get unknown, which seems surprising. Is this the expected behaviour? Are there options to improve the handling of such inequalities? I tried with and without configuration options, and various versions of Z3, including the current unstable branch. Any tips would be much appreciated!

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (> a 0))
(assert (> b 0))
(assert (> c 0))
(assert (<= a b))
(assert (not (<= (* a c) (* b c))))
(check-sat)
(assert (<= a (+ b 1)))
(assert (not (<= (* a c) (* (+ b 1) c))))
(check-sat)
Alex Summers
  • 256
  • 1
  • 8

1 Answers1

2

This falls into nonlinear integer arithmetic (which has an undecidable decision problem, see, e.g., How does Z3 handle non-linear integer arithmetic? ), so it's actually not too surprising Z3 returns unknown for some examples, although I guess a bit surprising that it toggled between unsat and unknown for quite similar examples.

If it works for your application, you can try a type coercion: encode the constants as Real instead of Int. This will allow you to use Z3's complete solver for nonlinear real arithmetic and returns unsat with check-sat.

Alternatively, you can force Z3 to use the nonlinear solver even for the integer encoding with (check-sat-using qfnra-nlsat) as in the following based on your example (rise4fun link: http://rise4fun.com/Z3/87GW ):

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (> a 0))
(assert (> b 0))
(assert (> c 0))
(assert (<= a b))
(assert (not (<= (* a c) (* b c))))
;(check-sat)
(check-sat-using qfnra-nlsat) ; unsat
(assert (<= a (+ b 1)))
(assert (not (<= (* a c) (* (+ b 1) c))))
; (check-sat)
(check-sat-using qfnra-nlsat) ; unsat

Some more questions and answers on similar subjects:

Combining nonlinear Real with linear Int

z3 fails with this system of equations

Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5

Can z3 always give result when handling nonlinear real arithmetic

Z3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)

Community
  • 1
  • 1
Taylor T. Johnson
  • 2,834
  • 16
  • 17
  • Thanks a lot for the quick answer! Replacing the Ints with Reals is interesting - I will have a think about when/where we could try that. Unfortunately, the problem comes from the context of a program verifier, in which somewhat arbitrary properties can show up in addition to this kind of arithmetic. So I'm not sure that we can soundly use the Real trick in general, unfortunately. Similarly, the (check-sat)s that we generate need in general to use many solvers, e-matching etc.. – Alex Summers Jan 28 '15 at 10:21