z3の各変数の値の範囲を制限できますか？

たとえば、私は制約x + y > 100を持っています。私はz3がxの値に1または2を与えることを望んでいません。そして、私はz3がyの値に1または2を与えることを望ましくありません。z3の各変数の値の範囲を制限できますか？

ので、xとyは1または2

以外の任意の番号にすることができ、我々はZ3のような制限を強制することはできますか？

ありがとうございます！

もちろん、単に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]

2017-02-01 01:08:43

だろう、私はそのような制限の倍数（ロット）のセットを持っている場合は、計算の複雑さにまで追加しますか？たとえば、 'n'の数が1、3、100などでないように' x'を指定し、 'n'を比較的大きくするとします。それは計算を大幅に遅くするだろうか？ –

試してみることができません：あなたの制約の複雑さにもよります。しかし、このような単純な比較であれば、z3がうまくいくと思います。それにショットをつけて、それが悪い場合にはそれをさらに見ることができます。 –

私はこれらの制約条件を後ろではなく正面に置くと、理論的には違うのですか？ –

答えて