Integer変数の特定のドメインをz3で取得する方法はありますか（変数が有限ドメインに属すると仮定します）。z3でIntのドメインを取得する
私は、制約の次のセットがあります。
1 <= X <= 5
2 <= Y <= 8
X + Y == T
をし、私が取得したいと思います：
あるいは単純ケース：
1 <= X <= 10
5 <= X <= 15
私が取得したいです：
5 <= X <= 10
これはかなり簡単なようですが、私はz3でそのような答えを得る方法を見つけませんでした。
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が応答するには：：;あなたは右の目を細めた場合、3 <= T <= 13を言っている、
sat
(objectives
(T 3)
)
sat
(objectives
(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を示します。今
(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)
：あなたはソルバーを2回呼び出しを避けたい場合は、あなたが独立して目標を最適化し、最適化するboxパラメータを、使用することができます
sat
(objectives
(T 3)
(T 13)
)
、すなわち、3のための最小限に抑え、13を最大化する。
私もこの解決策を考え出しました。問題は、変数ごとに呼び出す必要があり（1つは最大化し、1つは最小限にする）、変数がどのように拡大するのかということです。制約のセットはかなりシンプルなので、それぞれの呼び出しは簡単にソルバーにする必要がありますが、オプティマイザを使用するときに問題が発生しました（時間がかかりすぎる可能性があります） –
'box'パラメータを使用して単一呼び出しが可能です。編集された答えを参照してください。 –