1

現在、PythonでZ3を使用しています。レベルをプッシュして後でポップできるアサーションスタックを作成したいと思います。プッシュ操作とポップ操作を使用する他の「スタック」とまったく同じように機能するはずです。したがって、SMTLIB2標準では、2つの関数「push（n）」と「pop（n）」がオプションの数値nで定義されています。私の場合、nは常に1になります。

しかし、Z3には奇妙な振る舞いがあるようです。次のコードで「インデックスが範囲外」になるのはなぜですか？

s = Solver()
s.push()     # expected: one new level on the stack, reality: emtpy stack
s.pop(1)     # expected: stack is empty, reality: exception (index out of bounds)

アサーションを追加すると、Z3は期待どおりに機能します。

s = Solver()
s.push()
s.add(True)  # now there is one level on the stack,
s.pop(1)     # pop is successful

これでも正しく機能します：

s = Solver()
s.add(True)
s.push()     # now there is one level on the stack,
s.pop(1)     # pop is successful

問題は、プログラムで作成されるレベルとアサーションの数がわからないことです。アサーションがまったくなく、1つのレベルしかない可能性があります。その後、プログラムはクラッシュします（または例外をキャッチします）。回避策は、常に最初のステップとして「True」のような単純な式を追加することですが、これは醜いようです。

これはZ3のバグですか、それともこの動作は正しいですか？

4

1 に答える 1

1

unstableこのバグは、 （進行中の）ブランチで修正されています。次の公式リリースで利用できるようになります。それまでの間、不安定なブランチをコンパイルする方法についていくつか説明します。この修正は、 codeplexで利用可能なナイトリービルドでも利用できます。

于 2013-03-18T22:16:52.087 に答える