【发布时间】：2016-05-13 02:34:14
【问题描述】：
假设我有一些可以使用的公式，但我想获得更小（或更大）的可能值，所以请使用该公式。
有没有办法告诉 SMT 求解器给出那种小解？
例子：
a+1>10
在该示例中，我希望 SMT 求解器为我提供解决方案 10 而不是 100。
干杯
注意：我刚刚看到 similar question 的一位 z3 作者回答说，三年前，他们正在 z3 中实现该功能。你知道它是否已经实施了吗？
【问题讨论】：
【发布时间】：2016-05-13 02:34:14
【问题描述】：
可以使用maximize 和minimize More info 来完成
(declare-const x Int)
(assert (> (+ x 1) 10))
(minimize x)
(check-sat)
(get-model)
【讨论】：
-
这适用于 Z3 版本 4.4.1。它在 Z3 版本 4.3.3 中不存在，因此它是在这些版本之间的某个位置添加的。