得到SMT公式的较小模型

Question

假设我有一些公式可以被接受，但是我想得到更小的(或更大的)可能的值，所以这个公式。

有没有办法告诉SMT的求解者给出这种小的解决方案？

示例：

a+1>10

在这个例子中，我希望SMT求解器给我解决方案10而不是100。

干杯

注意:我刚刚看到一个相似问题，其中一个z3作者在三年前回答说，他们正在z3中实现这个功能。你知道它是否已经实现了吗？

Answer 1

这可以使用maximize和minimize 更多信息来完成。

(declare-const x Int)
(assert (> (+ x 1) 10))
(minimize x)
(check-sat)
(get-model)