Das kleinere Modell für eine SMT-Formel erhalten

Question

Lassen Sie uns sagen, dass ich einige Formeln habe, die gesessen werden können, aber ich möchte den kleineren (oder größeren) möglichen Wert bekommen, also saß diese Formel.

Gibt es eine Möglichkeit, dem SMT-Solver zu sagen, dass er eine solche kleine Lösung geben soll?

Beispiel:

a + 1> 10

In diesem Beispiel habe ich die SMT-Solver wollen die Lösung geben Sie mir 10 statt 100

Prost

HINWEIS: Ich habe Ich habe gerade eine similar question Antwort von einem der z3-Autoren gelesen, die vor drei Jahren sagten, dass sie diese Funktionalität in z3 implementiert haben. Weißt du, ob es bereits implementiert ist?

Answer 1

Es kann getan werden, maximize und minimizeMore info

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