Minimum and maximum values of integer variable

user_1217406 0
Viewed 4341

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.

z3
3 Answers

z3 now supports optimization.

from z3 import *

o = Optimize()
x = Int( 'x' )
o.add(And(x > 0, x < 5))
o.maximize(x)
print(o.check())  # prints sat
print(o.model())  # prints [x = 4]

This particular problem is an integer program.

user_24294260
Related