0

この質問は、これとこの質問に強く関連しています。

distinctZ3の機能

(declare-const a S)
(declare-const b S)
(assert (distinct a b))

セット内のすべての変数が異なる値を取る必要があるように、変数のセット (ここではaと) を制約できます。b

私の質問は次のとおりです。変数を区別する必要がある変数のセットを明示的に参照せずに、変数に一意の値を強制することもできますか? 何かのようなもの

(declare-unique-const a S)
(declare-unique-const b S)
(declare-unique-const c S)

これは、プログラムの検証中など、反復プロセスで新しい変数を宣言する状況で便利です。

それが不可能な場合は、すべての個別の変数を追跡し、そのセットを使用して適切なdistinct (newvar, oldvar1, ..., oldvarn))制約を発行する必要があると思います。

4

1 に答える 1

1

fからSへの補助的なフレッシュ関数を定義しInt、アサートすることができます

f(a_1) = 1
f(a_1) = 2
f(a_3) = 3
...
f(a_n) = n

次に、a_1、 ... はa_n互いに異なる必要があります。bそれもすべてとは違うと言いたいa_iのです。私たちはただ断言します

f(b) = n+1

このアプローチでは、カウンターを追跡するだけで済みます。

于 2013-02-19T16:16:22.763 に答える