Можем ли да ограничим диапазон от стойности за всяка променлива в z3?

Например имам ограничение x + y > 100. Не искам z3 да ми дава стойности на x да бъдат 1 или 2 и не искам z3 да дава стойности на y също да бъдат 1 или 2.

Така че x и y могат да бъдат произволно число освен 1 или 2.

Можем ли да наложим такова ограничение на z3?

Благодаря!


z3 z3py
person Fuxiang Chen    schedule 31.01.2017    source източник

Отговори (1)


arrow_upward
1
arrow_downward

Разбира се.. Просто заявете x > 2 AND y > 2. Ето го в z3py:

from z3 import *

x = Int('x')
y = Int('y')

s = Solver()
s.add (x > 2)
s.add (y > 2)
s.add (x+y > 100)

s.check()
print s.model()

Z3 отпечатва:

$ python a.py
[y = 3, x = 98]
person alias    schedule 01.02.2017
comment
Това би ли добавило към изчислителната сложност, ако имам множество (много) набори от такива ограничения? Например, ако искам x да не е 1, 3, 100 и т.н. за n брой термини и n е относително голям. Ще забави ли драстично изчислението? - person Fuxiang Chen; 01.02.2017
comment
Невъзможно да се каже, без да се опита: Зависи и от сложността на вашите ограничения. Ако обаче всички те са прости сравнения като това, сигурен съм, че z3 ще свърши добра работа. Опитайте го и ако се представи лошо, можем да го разгледаме по-подробно. - person alias; 01.02.2017
comment
Има ли различно (теоретично), ако поставя тези ограничителни ограничения отпред, а не отзад? - person Fuxiang Chen; 01.02.2017
comment
Редът не би трябвало да има значение, наистина. Бих искал да знам дали намирате друго. - person alias; 01.02.2017