如何为 z3 优化器设置超时，以便在超时时为您提供最知名的解决方案？
from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())
后续问题，你可以将z3设置为随机爬山还是始终执行完整搜索？
我正在使用带有内置 Gecode 6.1.1 的 minizinc，并且我希望最大化目标函数，其值远大于最大 int 32。32 位整数的最大值是 2147483646。虽然似乎没有太多信息与minizinc 参考文献中整数的最大值相关。然而，以下测试表明 Minizinc 使用 32 位整数。
测试非常简单，它只是尝试最大化 var int。
var int: maxInt;
constraint maxInt>0;
solve maximize maxInt;
output ["maxInt = \(maxInt)"];
结果是
最大整数 = 2147483646
结果接近最大 int32 值，而且 miniZinc 似乎无法进一步“最大化”它。以下示例返回一个奇怪的错误。
var int: maxInt;
constraint maxInt>2147483646;
solve maximize maxInt;
output ["maxInt = \(maxInt)"];
错误消息如下。该错误消息信息不多，但在尝试使用大于 2147483646 的数字时会显示。
错误：第 1 行中的整数文字无效。2 错误：语法错误，第 1 行出现意外的“,” 2 进程以非零退出代码 1 结束
我的问题如下：我可以在 minizinc 中使用 int64 位整数或任何其他大整数表示形式吗？如果可以，如何使用？（使用浮动不是一种选择）理想情况下，我想举一些例子来说明如何最大化某些东西
constraint maxLargeInt>2147483647;