z3 - Minimum and maximum values of integer variable

Question

Let's assume a very simple constraint: solve(x > 0 && x < 5).

Can Z3 (or any other SMT solver, or any other automatic technique) compute the minimum and maximum values of (integer) variable x that satisfies the given constraints?

In our case, the minimum is 1 and the maximum is 4.

Answer 1

Z3 has not support for optimizing (maximizing/minimizing) objective functions or variables. We plan to add this kind of capability, but it will not happen this year. In the current version, we can "optimize" an objective function by solving several problems where in each iteration we add additional constraints. We know we found the optimal when the problem becomes unsatisfiable. Here is a small Python script that illustrates the idea. The script maximizes the value of a variable X. For minimization, we just have to replace s.add(X > last_model[X]) with s.add(X < last_model[X]). This script is very naive, it performs a "linear search". It can be improved in many ways, but it demonstrates the basic idea.

You can also try the script online at: http://rise4fun.com/Z3Py/KI1

See the following related question: Determine upper/lower bound for variables in an arbitrary propositional formula

from z3 import *

# Given formula F, find the model the maximizes the value of X 
# using at-most M iterations.
def max(F, X, M):
    s = Solver()
    s.add(F)
    last_model  = None
    i = 0
    while True:
        r = s.check()
        if r == unsat:
            if last_model != None:
                return last_model
            else:
                return unsat
        if r == unknown:
            raise Z3Exception("failed")
        last_model = s.model()
        s.add(X > last_model[X])
        i = i + 1
        if (i > M):
            raise Z3Exception("maximum not found, maximum number of iterations was reached")

x, y = Ints('x y')
F = [x > 0, x < 10, x == 2*y]
print max(F, x, 10000)