Z3最大化API：可能的錯誤？

Question

我正在玩Z3（opt分支）的最大化API，並且我偶然發現了一個下面的bug：

每當我給它任何無限的問題，它只是返回給我OPT，並給出零得到的模型（例如最大化Real（'x'），而對模型沒有限制）。

Python的例子：

from z3 import * 

context = main_ctx() 
x = Real('x') 
optimize_context = Z3_mk_optimize(context.ctx) 
Z3_optimize_assert(context.ctx, optimize_context, (x >= 0).ast) 

Z3_optimize_maximize(context.ctx, optimize_context, x.ast) 
out = Z3_optimize_check(context.ctx, optimize_context) 
print out 

而且我得到的out值是1（OPT），而現在看來似乎應該是-1。

Answer 1

感謝您嘗試此實驗分支。 這些日子裏，開發仍然在不斷髮展，但大部分功能都相當穩定，您可以嘗試一下。

回答你的問題。有一種本地方式可以使用Z3的優化功能。 套用您的例子，這裏是什麼是相關的：

from z3 import * 

x = Real('x') 
opt = Optimize() 
opt.add(x >= 0) 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

當運行它，你會看到下面的輸出：

sat 
oo 
[x = 0] 

第一行說，斷言是滿足的。 第二行打印滿意度調用下的句柄「h」的值。

句柄的值保存滿足opt.maximize/opt.minimize調用聲明的最大化/最小化標準的表達式。 在這種情況下，表達式是「oo」。這有點「黑客」，因爲它將取決於你猜測「oo」意味着無窮大。如果你把這個值解釋回Z3，你將無法獲得無窮大。 （我在這裏限制使用Z3，我們不公開非標準數字，還有另外一部分Z3包含非標準數字，但這是另一回事）。

請注意，opt.maximize調用返回句柄「h」， ，後者用於查詢什麼是最優值。最後一行是滿足約束條件的一些模型。 當目標有界時，該模型將成爲您期望的模型，但在這種情況下，目標是無界的。 沒有有限的最佳值。

嘗試，例如，而不是：

x = Real('x') 
opt = Optimize() 
opt.add(x >= 0) 
opt.add(x <= 10) 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

這個時候你得到的將X = 10的模式，這也是最大的價值。

您也可以嘗試：

x = Real('x') 
opt = Optimize() 
opt.add(x >= 0) 
opt.add(x < 10) 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

輸出是現在：

sat 
10 + -1*epsilon 
[x = 9] 

小量指非基準數（無限）。你可以任意設置它很小。 該模型再次只使用標準數字，所以它挑選了一些數字，在這種情況下爲9.