問題タブ [z3py]

Z3Pyで、与えられた制約の方程式に解が1つしかないかどうかを確認するにはどうすればよいですか？

複数の解決策がある場合、どうすればそれらを列挙できますか？

次のスクリプトhttp://rise4fun.com/Z3Py/Cblの何が問題になっていますか？最後の2行を追加すると、次のエラーが発生します'instancemethod' object is not #subscriptable

z3pyをアプリケーションに統合しようとしています。次のような小さな実数を含むアサーションがあります

次に、次のエラーが発生しました。

アサーション中

大丈夫そうです。

したがって、z3にはある種の精度制限があると思います。もしそうなら、最初のアサーションを通過させるオプションはありますか？

ありがとう。

方程式ペルを持っているx*x - 193 * y*y = 1

z3pyの場合：

結果：[y = 2744248620923429728, x = 8169167793018974721]

なんで？

PS有効な答え：[y = 448036604040、x = 6224323426849]

Z3モデルから実際のPython値を取得するにはどうすればよいですか？

例えば

プリント

ただし、これらはZ3オブジェクトであり、python float/boolオブジェクトではありません。

is_true/を使用してブール値を確認できることは知っていますが、int / reals / ...を使用可能な値にエレガントに変換するにはどうすればよいですか（たとえば、is_false文字列を調べたり、この余分な記号を切り取ったりする必要はありません）。?

以下の例に示すように、Z3 Python インターフェイスは ** 演算子が好きではないようです。x*x は処理できますが、x**2 は処理できません。

print solver.model()次のプログラムは、マスター git ブランチ (commit 89c1785b) の最新バージョンの Z3 を使用して、印刷できない (つまり、例外をスローする) Z3 モデルを生成します。

生成:

http://rise4fun.com/Z3Py/lfQGのオンライン z3py インターフェイスでも同じ動作を再現できます。もう少しデバッグすると、モデルの割り当てcが、z3.FuncInterp呼び出し時に「無効な引数」例外をスローするものであることが示唆else_value()されます。

これは Z3 のバグですか、それとも私の予想が正しくないのでしょうか? 私の期待は、それ以外の場合は完全な関数ではないため、else_value()a のを常に取得できるはずですが、おそらくこれは常に正しいとは限りませんか?FuncInterp

Z3Py には式があります。数式で使用して変数のリストを取得するにはどうすればよいですか?

ありがとう。

私はZ3 pythonでこのコードを持っています:

しかし、このコードは実行時に以下のエラーを報告します:

xorに置き換えればand問題ありません。これは、XOR がサポートされていないことを意味しますか?

Z3 pythonの配列理論を使用したコード例を探していますが、見つかりません。

誰かがいくつかのコード例を提供してもらえますか？

ありがとう！