獲取SMT公式的較小模型

Question

假設我有一些可以坐下的公式，但我希望得到較小（或更大）的可能值，以便坐在那個公式中。

有沒有辦法告訴SMT解算器給這種小解決方案？

實施例：

一個+ 1> 10

在那個例子中我想要的SMT求解器來給我溶液的10代替100

乾杯

注：我有剛剛看到一個similar question由z3的作者之一在三年前回答說，他們正在z3中實現該功能。你知道它是否已經實施？

Answer 1

它可以通過maximize和minimizeMore info

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