z3 - Z3 で解や探索空間を指定できますか?

Question

私の質問を例で説明しましょう：

たとえば、-1、0、2、3、5、および 6 などの可能な離散整数の領域があるとします。ここで、次の制約を満たす変数 x の解 (またはモデル) を探しています。

(x > 0) && (x < 6) && (x != 3) && (x > 2)

答えは (ソリューション ドメインから) = 5 になりますね。

Z3でこれを行うにはどうすればよいですか？

つまり、個別のエンティティを使用して解空間を定義し、いくつかの制約をアサートして、Z3 に充足可能性を確認するように依頼します。満足できる場合は、モデルが必要です。

誰かが例を手伝ってくれますか?

ありがとう、イシュティアク

Answer 1

x == -1 || x == 0 || x == 2 || x == 3 || x == 5 || x == 6事前に公理としてそれを行うべきであると主張します。Z3にもっと良い方法が組み込まれているかどうかはわかりません。

編集：私は以前に使用したことがありませんが、別の解決策は配列を使用することかもしれません。A概念的には、数値を含む配列を宣言して、次のように言うことができるはずです。

(exists (y Int) (=(select A y) x))`

これまで配列を使用したことがないため、それが正確な構文であるかどうかはわかりませんが、うまくいくはずです。