Abrufen der Domäne eines Int mit z3

Question

Gibt es eine Möglichkeit, die spezifische Domäne einer Integer-Variablen mit z3 zu erhalten (unter der Annahme, dass die Variable zu einer endlichen Domäne gehören)?

Ich habe folgenden wird die von Einschränkungen festgelegt:

1 <= X <= 5 
2 <= Y <= 8 
X + Y == T 

und ich würde erhalten mag:

3 <= T <= 13 

oder auch einen einfachen Fall:

1 <= X <= 10 
5 <= X <= 15 

Ich will bekommen :

5 <= X <= 10 

Das scheint ziemlich trivial zu sein, aber ich habe keine Möglichkeit gefunden, eine solche Antwort mit z3 zu erhalten.

Answer 1

Sie können die Optimierungsroutinen von Z3 verwenden, um diese Art von Einschränkungen zu lösen. Ihr erstes Problem kann codiert werden, wie:

(declare-const X Int) 
(declare-const Y Int) 
(declare-const T Int) 
(assert (<= 1 X 5)) 
(assert (<= 2 Y 8)) 
(assert (= (+ X Y) T)) 

(push) 
(minimize T) 
(check-sat) 

(pop) 
(maximize T) 
(check-sat) 

Welche z3 antwortet:

sat 
(objectives 
(T 3) 
) 
sat 
(objectives 
(T 13) 
) 

Welche, wenn Sie mit dem rechten schielen, sagt 3 <= T <= 13; als du versucht hast es herauszufinden.

Sie können auch die Python-Schnittstelle verwenden, um dasselbe zu tun. Ihr zweites Beispiel kann in z3py wie folgt codiert werden:

[X = 5] 
[X = 10] 

anzeigt 5 <= X <= 10:

from z3 import * 

X = Int('X') 

s = Optimize() 

s.add(1 <= X); s.add(X <= 10) 
s.add(5 <= X); s.add(X <= 15) 

s.push() 
s.minimize(X) 
s.check() 
print s.model() 

s.pop() 
s.maximize(X) 
s.check() 
print s.model() 

die produziert.

Erste min/max mit einem Anruf

Wenn Sie zwei Anrufe an den Solver vermeiden wollen, dann können Sie den box Parameter Optimierung verwenden, die unabhängig voneinander die Ziele optimiert:

(declare-const X Int) 
(declare-const Y Int) 
(declare-const T Int) 
(assert (<= 1 X 5)) 
(assert (<= 2 Y 8)) 
(assert (= (+ X Y) T)) 
(minimize T) 
(maximize T) 
(set-option:opt.priority box) 
(check-sat) 

Jetzt , z3 antwortet:

sat 
(objectives 
(T 3) 
(T 13) 
) 

, die die Ergebnisse in der Reihenfolge enthält gegeben, dh 3 für minimieren und 13 für maximieren.