Получение модели меньшего размера для формулы 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)