Получение домена Int с z3

Question

Есть ли способ получить конкретный домен переменной Integer с z3 (при условии, что переменная принадлежит к конечной области)?

Я следующий набор ограничений:

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

, и я хотел бы получить:

3 <= T <= 13 

или даже более простой случай:

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

Я хочу, чтобы получить :

5 <= X <= 10 

Это кажется довольно тривиальным, но я не нашел способ получить такой ответ с помощью z3.

Answer 1

Вы можете использовать подпрограммы оптимизации Z3 для решения этих ограничений. Ваша первая проблема может быть закодирован как:

(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) 

На что z3 отвечает:

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

Что, если вы косоглазие право, говорит 3 <= T <= 13; как вы пытались это выяснить.

Вы также можете использовать интерфейс Python, чтобы сделать то же самое. Ваш второй пример может быть закодирован в z3py следующим образом:

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() 

, который производит:

[X = 5] 
[X = 10] 

с указанием 5 <= X <= 10.

Получение мин/макс одним вызовом

Если вы хотите, чтобы избежать двух вызовов в решатель, то вы можете использовать параметр box для оптимизации, который оптимизирует цели независимо друг от друга:

(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) 

сейчас , z3 отвечает:

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

, который содержит результаты в указанном порядке, то есть, 3 для минимизации и 13 для максимизации.