Можем ли мы ограничить диапазон значений для каждой переменной в 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