2

私は Z3 を初めて使用し、そのビットベクター C++ API を使用しようとしています。私が理解している限り、クラスコンテキストのメソッド bv_val(int n, unsigned sz) は、値 n でサイズ sz のビットベクトルを作成することを目的としています。しかし、値 n が int 型に制限されているのはなぜですか? サイズ 10 のビットベクトルを値 (たとえば 2^64 より大きい) で作成するとどうなりますか?

誰かが私にいくつかの提案をしてくれますか?. 前もって感謝します。

4

2 に答える 2

0

おそらく、この質問に対する唯一の答えは、「開発者がそうしたからです」というものです。

コンピューター サイエンスでは、有限の量しか表現できません。API を設計するとき、何かの最大値または最小値がどうあるべきかという疑問が生じることがあります。この特定のケースでは、 の最大値は のnようですUINT_MAX(unsigned int関数のオーバーロードがあります)。

おそらく、開発者はユースケースn > UINT_MAXが非現実的だと考えていたのでしょう。正気の誰もそれを試みないだろうということ。

操作を実行するとn > UINT_MAX、リソースに負担がかかりすぎた (時間がかかりすぎた、メモリが多すぎた) ためである可能性があります。

おそらく、この種の操作を複数の部分に分割する方法があり、1 つの大きなパスで実行できないことが問題にならないためです。

あるいは、誰かがそれについて考えていなかっただけで、合格する必要性がn > UINT_MAX本当に存在しているのかもしれません. その場合は、バグ トラッカーに問題を送信していただけると思います。

ほとんどの場合、誰かが「もう十分だ」と考えたからです。いずれにせよ、この質問は本当に答えられません。

于 2013-06-26T18:23:30.483 に答える