普遍的な定量化変数の境界付け

Question

Z3で普遍化された変数の値の範囲を束縛することが可能かどうかを知りたいと思います。

たとえば、システムの時間をモデル化するために使用される「time」というタイプの変数があるとします。 私は単項関数 "func1"の値は常に1から100の間でなければならないという主張を持っているとしましょう。関数は入力に時間変数をとります。 Z3で表すと、私は次のようにプロパティをコード化している：

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

   私は明示的に私はZ3は私が注入場合UNSAT私を与える行きたいので、普遍的に定量化するために時間変数が必要であることに注意してください次のタイプのプロパティ：

2. 限り私の理解がZ3のために行くように、すべての定数は、数学的（理論値）といないコンピュータ（実用的）イムを持っていますつまり、それらの値は束縛されません（残念ながら、私は現時点でこれを読んだリソースを指摘できません）。私のシステムで時間をモデル化し、システムの制約に従って、x時間以上実行することはできないと仮定します。これは、時間の値が0とx * 60 '* 60の間で最大である実行時間（秒単位）。私は、次のアサーションとの時間のために許可された値を主張することができることを知っている：

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

   が、それは1で与えられた普遍的定量化に影響を与えるのだろうか？

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

Answer 1

ただし、1）の普遍的な定量に影響しますか？

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

はバウンドとして "時間" 変数を扱うことに注意してください。あなたは上記をアサートすると、意味がXXのいずれかのインスタンス化は、（がアサートされている）を保持していることである

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

：式が同じ意味を持っています。具体的には、あなたが自由変数「時間」を数量化変数をインスタンス化することができ、特に、あなたは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))) 

を（残念ながら私はPOIすることはできません私は現時点でこれを読んでいるリソースにnt）。

妥当な論理テキストブックまたはコンピュータサイエンスブックの基礎は、これを深く説明する必要があります。 Z3は、標準的な1次多ソートロジック（バックグラウンド理論を使用）をサポートしています。