我們可以限制z3中每個變量的一系列值嗎？

Question

例如，我有一個約束x + y > 100。我不想讓z3將x的值設爲1或2，並且我不希望z3將y的值設爲1或2。

因此，x和y可以是任意數量的除了1或2

我們可以Z3執行這樣的限制？

謝謝！

Answer 1

當然..簡單地聲稱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]