2017-03-22 7 views
0

私はソルバーの関数を使って離散時間をモデル化しています。問題は今はz3.Function('f', IntSort(), IntSort())のような関数を使用し、関数への負の入力値は時間がt = 0で始まるため実際には適用できないということです。これは、ソルバーが負の時間の解決策を見つけることが全く考慮されていないので、私が物事をprooveしたいときに問題を引き起こします。Z3にUnsignedIntSortはありますか?

私の質問は:z3には何らかの種類の符号なしint sort(UnsignedIntSort)がありますか?

+1

私はそのような並べ替えを認識していません。しかし、 'unsigned int '型であるべき各定数(または関数)に' 0 <= x'という制約を追加することはできませんか? –

答えて

0

コメントに指摘されているように、このような並べ替えはありません。あなたのベスト・ベットは、すべての用途に対してアサーションがt >= 0であることを確認することです。

実際にはこれは実際にはトリッキーです。すべての "新鮮な"変数に対してこのアサーションを行う必要があるだけでなく、結果がドメイン内に残っていることを保証するためにそのような変数を使って算術演算を行うたびにもアサーションを行う必要があります。つまり、t-1を計算した場合、その式の結果が時間値として使用されていると仮定すると、アサーションが表示されます。t >= 1が必要になります。

これは本当に面倒で本当に面倒なので、メカニズム(「過負荷算術」)を持つことで人生を簡素化できます。もちろん、これは、SMT-Libを使用しているか、より高度な言語を使用してAPIを使用しているかにかかわらず、制約をどのようにプログラミングするかによって異なります。

+0

私はPython APIを使用しています。 Unsignedが利用できない場合は、代わりに 'Enum〜range(2000)'を使用します。 – Moberg

0

SMTまたはZ3に符号なしソートはありません。これは、ビットベクトルを簡単にこの目的で使用できるためです。ビットベクトルのヘルスセルは符号なしでも符号付きでもありませんが、ビット列です。符号付きおよび符号なしセマンティクスは別々の関数で実装されます。つまり、ビットベクトル用のより小さい演算子はありませんが、符号なしと符号なしの場合はbvultbvsltがあります。したがって、すべてのBV関数の符号なしのフレーバーに固執する限り、符号なしセマンティクスは常に保持されます。

また、モデルでは、ビットベクトルは通常、ビット列(バイナリまたは16進数)として提供されます。つまり、負の値はありません。アプリケーションでは、*s*関数の使用を開始するまで、すべてのビットベクトルが符号なしであると常に仮定できます。

+1

ビットベクトルの問題は、もちろん、算術演算が重複していることです。 8ビットベクトルの場合は '0-1 == 255'。例えば。おそらく無限の数量としてモデル化されるはずの、時間のようなものをモデル化するためのショーストッパーとなるかもしれません。 –

関連する問題