获取 SMT 公式的较小模型 [英] Getting the smaller model for a SMT formula

问题描述

假设我有一些可以设置的公式，但我想获得更小(或更大)的可能值，因此请设置该公式.

Let say that I have some formulas that can be sat but I want to get the smaller (or larger) possible value so sat that formula.

有没有办法告诉 SMT 求解器给出那种小的解决方案?

Is there a way to tell the SMT solver to give that kind of small solution?

示例:

a+1>10

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

In that example I want the SMT solver to give me the solution 10 instead of 100.

干杯

注意:我刚刚看到一个类似的问题z3 作者说，三年前，他们正在 z3 中实现该功能.你知道它是否已经实施了吗?

NOTE: I have just seen a similar question answered by one of the z3 authors saying, three years ago, that they were implementing that functionality in z3. Do you know if it is already implemented?

推荐答案

可以使用 maximize 和 minimize 更多信息

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

这篇关于获取 SMT 公式的较小模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！