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.