3

Z3 is able to derive boolean consequences of the theory as explained in https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences

Now I am wondering whether it is possible to also do this for numeric values. For instance given the following theory:

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= (+ x y) 10))
(assert (and (>= y 20) (>= x -20)))
(check-sat)
(get-model)

I am wondering whether it is possible to derive that "y" must lie between 20 and 30, and x must lie between -20 and -10.

The one workaround I can come up with is maximizing and minimizing these variables and then I would get the range of possibilities, but it seems to me that there can be better ways of doing this.

Ingdas
  • 1,446
  • 1
  • 11
  • 21

1 Answers1

2

This is quite similar to a previous stack-overflow question: Using SMT-LIB to count the number of modules using a formula

Bottom line: If there is more than one variable involved, then this problem is really hard to solve in general; unless you use specific knowledge of the problem. If there's precisely one variable, then you can indeed use optimization and other tricks to give you "ranges", but in general such an algorithm will not necessarily be performant. (Though in practice it can handle most simple things easily.)

If you do not care about discontinuities and only want to find out max/min, you can use z3's optimizer. Note that this is not part of standard SMTLib but rather a z3 extension. Here's an example:

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= (+ x y) 10))
(assert (and (>= y 20) (>= x -20)))

(assert (distinct x (- 15)))
(assert (distinct y 25))

(push) (minimize y) (check-sat) (get-objectives) (pop)
(push) (maximize y) (check-sat) (get-objectives) (pop)
(push) (minimize x) (check-sat) (get-objectives) (pop)
(push) (maximize x) (check-sat) (get-objectives) (pop)

This prints:

sat
(objectives
 (y 20)
)
sat
(objectives
 (y 30)
)
sat
(objectives
 (x (- 20))
)
sat
(objectives
 (x (- 10))
)

So, you can get the bounds but notice how the requirements I added that x != -15 and y != 25 are simply outside the ranges you get.

Note that if your type is unbounded (such as Int) you can also get +/- infinity as a bound:

(declare-const x Int)
(assert (< x 10))
(push) (minimize x) (check-sat) (get-objectives) (pop)
(push) (maximize x) (check-sat) (get-objectives) (pop)

This prints:

sat
(objectives
 (x (* (- 1) oo))
)
sat
(objectives
 (x 9)
)

Optimization is a hard problem in general, and the optimizing solver in z3 is definitely slower compared to the regular one. But it might just do the trick for your problem domain!

alias
  • 28,120
  • 2
  • 23
  • 40
  • 1
    Thank you for the pointer. However I feel that my case is different as I am asking a question which is already supported for the boolean case. I suppose that Z3 does some bounds reasoning internally and has some of this information available in an internal API. Is it possible to get this information out? (through a C++ call for instance?) – Ingdas Feb 20 '19 at 13:20
  • The optimizer keeps track of bounds, but keep in mind that it won’t tell you that it is valid for all points in the range. (There might be discontinuities.) that’s the main reason why this problem is really hard. – alias Feb 20 '19 at 14:27
  • I would love to obtain that kind of information, even when I know there might be discontinuities. Can you point me to the place where I can extract this out of the optimizer? – Ingdas Feb 21 '19 at 11:57
  • Sure; added a few examples on how to get the bounds with the caveat that discontinuities will be problematic. – alias Feb 21 '19 at 16:07
  • I truly appreciate the effort, thank you. I think that will do the trick for my problem domain but I have one more question for if it doesn't. Is it possible to get the internal estimate out of the solver through a call to the internal API? I suppose the internal propagators of Z3 will keep track of bounds at any point in time, without the guarantee that there is an actual solution for these bounds. These could serve as a low-cost overestimation of the solution space. – Ingdas Feb 22 '19 at 11:48
  • 1
    Check out [Z3_optimize_get_lower](https://z3prover.github.io/api/html/group__capi.html#ga1c754dd577a3c138bd12badb0c2f1ad9), [Z3_optimize_get_upper](https://z3prover.github.io/api/html/group__capi.html#ga658c4858c031d5affffcea9f857636fd) etc. I haven't personally used these myself, so I cannot comment on how easy to use or reliable they are in practice. – alias Feb 22 '19 at 14:33