Z3 Not Showing Infinity on Unbounded Optimization in Python

Question

I am new to Z3 and trying the examples found here, implementing the examples in python. When I try the examples in the "Unbounded Objectives" section I get seemingly random integer values (not 'oo'). For the following code:

x, y = Ints('x y')
opt = Optimize()
opt.add(x < 2)
opt.add((y - x) > 1)
opt.maximize(x + y)
print(opt.check())
print(opt.model())

I get the output:

sat
[y = 5, x = 1]

But the problem is unbounded, I expect it to give me y equal to infinity. A more simple example:

x, y, profit = Ints('x y profit')
opt = Optimize()
opt.add(profit == 2*x + y)
opt.maximize(profit)
print(opt.check())
print(opt.model())

This example gives me:

sat
[x = 0, y = 0, profit = 0]

My question is: Why am I not getting infinity here? Am I doing something wrong or is this the output I should expect from Z3 with python when I give it an unbounded optimization problem?

I am using python 3.9 on Pycharm 2021.2.1, Z3 version 4.8.15.

Answer 1

You're not quite using the API correctly. You should use the value function on the optimization goal instead. For instance, your second query is coded as:

from z3 import *

x, y, profit = Ints('x y profit')
opt = Optimize()
opt.add(profit == 2*x + y)

maxProfit = opt.maximize(profit)

print(opt.check())
print("maxProfit =", maxProfit.value())

This prints:

sat
maxProfit = oo

Note that when the optimization result is oo, then the model values for x/y/profit etc., are irrelevant. (They are no longer integers.) If the optimization result is a finite value, then you can look at opt.model() to figure out what assignment to your variables achieved the optimal goal. So, the values of x/y and profit you get in your example, while printed as 0, are meaningless; since the goal is not a proper integer value.