問題タブ [z3py]

私の質問は次のようなものです: Z3: Z3py 式を SMT-LIB2 に変換しますか?

z3py 式を smtlib2 形式に変換しようとしています。次のスクリプトを使用しますが、結果を z3 またはその他の SMT にフィードしているときに変換すると、次のようになります。

「構文エラー、予期しない let」

長い式を再度記述する必要がないように、z3py を使用して smtlib2 形式にする方法はありますか。

以下は、変換に使用しているコードです。

これは出力です：

私はz3pythonでpythonの数学ライブラリを使おうとしていましたが、私がしたことは

返されるエラー メッセージは AttributeError: ArithRef インスタンスに属性 ' float ' がありません。

私の目的は実際には Z3 で階乗関数を使用することではなく、数学ライブラリの関数が一般的に Z3 で使用できるかどうかに興味があります。どんな提案でも大歓迎です。

returns sat, and gives the solution

which does not satisfy the constraints. If I remove the final constraint, it returns a sensible pair that satisfies the first two (trivial) constraints. What's going on?

Permalink to try this online: http://rise4fun.com/Z3Py/fk4

EDIT : I'm new to z3, so there's a chance I'm doing something horribly wrong, do let me know.

Z3 で与えられた一般的なトポロジーの定理を証明しようとしています。

TPTP トポロジ

次のZ3-SMT-LIBコードを使用して、そこにあるコードを翻訳しています

対応する出力は

この例をここでオンラインで実行してください

最初satは正しいです。しかし、2 番目satは間違っていますunsat。つまり、Z3 は定理とその否定が同時に真であると言っているのです。

この場合どうなるか教えてください。どうもありがとう。ではごきげんよう。

2*2 オーダーの 2 つの行列を乗算しようとしています。行列の 1 つに未知のパラメータ "k1" が含まれています。k1のどの値に対して満足できる解を確認したい。2 つの行列の積は、3 番目の行列と等しくなります。注：乗算を行列として操作したい線形関係または方程式のセットに変換したくありません。

ここが私が立ち往生している場所です。

方法はありますか？

Z3Py で別の代数データ型に依存する代数データ型を作成できるかどうか疑問に思っています。

例として、独自の Bool データ型を定義し、Bool のリストを自分で定義したいとします。

これはうまくいきます：

これは次のメッセージで失敗します。

その理由は、以前に定義されたデータ型への参照として Bool() が使用されているためです。代わりに Z3 ブールソートを使用すると、魅力的に機能します。

別の代数データ型に依存する代数データ型の定義は不可能ですか、それとも s.th を渡す必要がありますか? Bool() 以外？

前もって感謝します！カルステン

リバース エンジニアリングの演習の一環として、以下のプログラムを満たすユーザー名とパスワードを見つける Z3 ソルバーを作成しようとしています。誰もが参照している z3py チュートリアル (rise4fun) がダウンしているため、これは特に困難です。

バイナリのアセンブリからそのコードを取得しました。間違っているかもしれませんが、ソルバーの作成に集中したいと思います。最初の部分から始めて、 を計算するだけですr1。これが私が持っているものです:

私が主張しているのは、配列に「A」未満の文字がないということだけです。そのため、65 より大きい数値を持つ任意のサイズの配列が返されることを期待しています。

主に無限ループであるため、明らかにこれは完全に間違っています。また、合計が 0 に初期化されているかどうかわからないため、合計を正しく計算しているかどうかもわかりません。誰かがこの最初のループを機能させる方法を理解するのを手伝ってくれますか?

編集:上記の C++ コードに近い z3 スクリプトを取得できました。

このコードにより、正しいユーザー名とパスワードを得ることができました。ただし、ユーザー名には 1、パスワードには 5 の長さをハードコーディングしました。長さをハードコードする必要がないように、スクリプトを変更するにはどうすればよいですか? また、プログラムを実行するたびに異なるソリューションを生成するにはどうすればよいでしょうか?

Z3py の Exists 関数を別の変数と数式で呼び出すと、まったく同じ結果が得られます。それはある種のPythonの問題ですか、それともZ3がここで壊れていますか? 直し方？次の最小限の例は、問題を示しています。

出力：