z3 - z3py 式の簡略化

Question

z3py を使用して式を単純化しようとしていますが、さまざまな戦術に関するドキュメントが見つかりません。私が見つけた最良のリソースは、すべての戦術を名前別にリストしたスタック オーバーフローの質問です。

利用可能な戦術に関する詳細なドキュメントに私をリンクさせることができる人はいますか? オンラインの python チュートリアルでは不十分です。

または、誰かがこれを達成するためのより良い方法を推奨できますか?

問題の例は、次のような式です。

x < 5, x < 4, x < 3, x = 1これを に簡略化したいと思いx = 1ます。

この例では、タクティックの使用unit-subsume-simplifyが機能しているように見えます。

しかし、結果としてx > 1, x < 5, x != 3, x != 4得x > 1, x < 5, x ≠ 3, x ≠ 4られるようなより複雑な例を試してみると。ご希望の際はx = 2。

z3py を使用してこのタイプの単純化を達成するための最良のアプローチは何ですか?

私の現在の解決策。

ありがとうマット

Answer 1

考えられる解決策:

x = Int('x')
s = Solver()
s.add(x < 5, x < 4, x < 3, x == 1)
print s.check()
m = s.model()
print m
s1 = Solver()
s1.add(x > 1, x < 5, x != 3, x != 4)
print s1.check()
m1 = s1.model()
print m1

出力：

sat
[x = 1]
sat
[x = 2]

ここでこのソリューションをオンラインで実行します

Answer 2

Reduce の Redlog を使用した例。どう思うか教えてください。