2

Z3 で普遍的に量化された変数の値の範囲を制限できるかどうかを知りたいです。

たとえば、システム内の時間をモデル化するために使用される「time」と呼ばれる Real 型の変数があるとします。ある単項関数「func1」の値は常に 1 から 100 の間でなければならないというアサーションがあるとします。関数は入力を時間変数とします。Z3 で表現すると、次のようにプロパティをエンコードしました。

  1. ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

    次のタイプのプロパティを注入すると、Z3 で unsat が返されるようにするため、時間変数を普遍的に定量化する必要があることに注意してください。

  2. Exists(time, func1(time) == 101)

    Z3 に関する私の理解では、すべての定数は数学的な (理論上の) 実装であり、コンピューターによる (実用的な) 実装ではありません。時間を使用してシステムの時間をモデル化し、システムの制約に従って x 時間以上実行できないと仮定します。これを使用して、時間の値が 0 から x*60'*60 の間で最大値を与えることができます。秒単位の実行時間。次のアサーションを使用して、時間の許容値をアサートできることを知っています。

  3. And(time >= 0, time <= x*60*60)

    しかし、それは1で与えられた普遍的な数量化に影響を与えますか?

したがって、これは、プロパティ 2 が注入され、指定した時間の値に対して が設定されている場合、 は時間の値に対してのみ有効であるため、x*60*60 + 1設定を解除すべきではないという状況につながるはずです。ForAll

4

1 に答える 1

1

しかし、それは1)で与えられた普遍的な数量化に影響を与えますか?

ご了承ください

ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

変数「time」をバインドされたものとして扱います。この式は、次と同じ意味です。

ForAll(xx, And(func1(xx) >= 1, func1(xx) <= 100))

上記をアサートすると、xx のインスタンス化が成立する (アサートされる) という意味になります。特に、量化された変数を自由変数「時間」でインスタンス化できます。特に、アサーションを生成する x*60*60+1 でインスタンス化できます。

 And(func1(x*60*60+1) >= 1, func1(x*60*60+1) <= 100)

あなたがそれを言いたかったとします。

 And(func1(xx) >= 1, func1(xx) <= 100))

0 から x*60*60 までのすべての値 xx が成り立つ場合、次のように記述できます。

ForAll(xx, Implies(And(xx >= 0, xx <= x*60*60), And(func1(xx) >= 1, func1(xx) <= 100)))

（残念ながら、現時点でこれを読んだリソースを指すことはできません）。

理にかなった論理の教科書やコンピュータ サイエンスの基礎書では、これについて詳しく説明する必要があります。Z3 は、標準的な一次多ソート ロジックをサポートします (背景理論を使用)。

于 2016-04-19T14:30:09.660 に答える