問題タブ [z3py]

Z3 でブール式の自動簡略化を無効にすることはできますか?

たとえば、式 2 > 1 は、2 > 1 のままにしたいのですが、自動的に True になります。

Z3Py で help_simplify() を呼び出して、いくつかのオプションを見つけました。しかし、それらのどれも私の問題に関連していないようです。

別のチュートリアル ( http://citeseerx.ist.psu.edu/viewdoc/download?rep=rep1&type=pdf&doi=10.1.1.225.8231 ) では、オプション "CONTEXT SIMPLIFIER" が言及されています。 -数式を真または偽にします。" ただし、Z3Py ではこのオプションを見つけることができませんでした。

背景: And(2>1, 1!=2) のような式を使用できるようにしたいと考えています。ここで、2>1 と 1!=2 は以前に自動的に生成され、変数 (定数) を含まない場合があります。Z3Py はこれを And(True, False) に簡略化しますが、これは受け入れられません。これは、「引数の少なくとも 1 つが Z3 式またはプローブでなければならない」ためです。したがって、簡素化は抑えたいと思います。または、And(True, False) を受け入れられる式にする方法はありますか?

前もって感謝します！

Z3 で「for all」を正しく使用する方法を誰かが教えてくれませんか。ドキュメントを調べましたが、情報が見つかりませんでした。私がやろうとしていることは

「foo」内で、Z3で次のことを言う必要があります

"let (u,r) be runnable(t) in { (assert ((u,r) is in users) (assert (r,t) is in roles)) }"

私が知らないのは、ランナブルの最初の要素を取得してユーザーにあることをアサートし、2 番目の要素をロールにあることをアサートする方法です。

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) ) ブール)

(assert (forall (t タスク)) (foo))

(check-sat) (get-model)

Python インターフェイスを介して Z3 を使用して、単純な線形式の充足可能性を推測しようとしています。smt2形式で書き留めた次のような単純な式（それぞれ10個の項を持つ10個の節で構成されています）でもかなり遅いようです：

次のコード ブロックを使用して、これらの式を動的に生成しています: )、変数の係数 (整数))。

私が抱えている問題は、Z3 がそのような公式に固執していることです。formula.smt2 という名前のファイルに保存し、bash Z3 コマンドで解決しようとすると、スタックしているようにも見えます。

私が使用しているソルバーのバージョンは次のとおりです。Z3 バージョン 4.3.2

使用しているフォーマットが不便ですか、それとも Z3 のせいですか? 解決プロセスをスピードアップするために使用できるトリックはありますか?

Juan Ospina が提案したように、数式のどの部分がソルバーにとって難しい部分であるかを把握しようとしました。以下のようです。

実際、この式から任意の句を削除すると、ソルバーは 1 秒以内に応答できますが、式全体を入力すると時間切れになります。

なぜこれが起こるのですか？Z3がこの式を解くのがとても難しいと思うのは普通ですか?

ベスト、アンドレア

Z3 によって生成されたモデル値の結果のランダム性に影響を与えようとしています。私が理解している限り、これに対するオプションは非常に限られています。線形演算の場合、シンプレックス ソルバーは、指定された制約を満たすランダムな結果を許可しません。ただし、オプション smt.arith.random_initial_value (「線形演算のシンプレックスベースの手順でランダムな初期値を使用する (デフォルト: false)」) があり、これは機能していないようです:

これは結果として常に [y = 0, x = 1] を生成するようです。特定の制約で使用されていない変数のモデル補完でさえ、常に決定論的な結果を生成するようです。

このオプションがどのように機能するかについてのアイデアやヒントはありますか?

Google アプリ エンジンで z3 を実行するのに役立つ純粋な python z3 パッケージを見つけたいと思います。次のpythonテストをローカルで実行しましたが、実行されます：

ただし、動作させるには次のファイルが必要です: z3.pyc、z3consts.pyc、z3core.pyc、z3printer.pyc、z3types.pyc、libz3.dylib。これらのファイルは、z3 codeplex サイトからのダウンロードから z3 をビルドすることで取得しました。

したがって、アプリIDフォルダー内の「lib」フォルダーにあるこれらのファイルを使用して、main.py（Googleが提供する「hello world」プログラム）の次の適応を試みました。

このコードをアプリ エンジン ランチャーで実行すると、空白のページが表示され、エラー メッセージは表示されません。

z3 関連のコードをすべてコメント アウトすると、予想どおり、Hello World メッセージが表示されます。

注: サード パーティのライブラリを含める方法に関する記事 14850853 を読み、BeautifulSoup を使用して正常にテストしました。私の質問は、純粋な python z3 ライブラリの可用性についてです。

サンドボックスに関する Google のドキュメントから、*.pyc ファイルは問題ないと確信していますが、これらのファイルが機能するために必要な (16MB) libz3.dylib は純粋な python ではないと思います。z3 の純粋な Python バージョンは存在しますか、それともアプリ エンジンで z3 を使用する他の方法がありますか?

v4.3.1 としてタグ付けされた Codeplex の最新の z3 マスター コードを使用しています。

prove有用な戻り値を持ち、印刷されないような関数が必要です。だから、私は明らかだと思われることを書きました：

ただし、このコードの実行はデフォルトの関数よりも大幅に遅くなりますprove。

prove(slimmed)のコードsrc/api/python/z3.pyは次のとおりです。

s.set()コードに追加すると、高速で同じ反例が見つかります。

ここで何が起こっているのですか？

• s.set()一般的に悪いいくつかのオプションを何らかの方法でクリアするためのその空の呼び出しはありますか?
• ..私の特定のテストには悪いですか？
• 他の何か？

デフォルトのソルバー オプションが何であるかを調べようとしましたがstr(s) repr(s)、 、s.__dict__、および google はあまり役に立ちませんでした。

どんなアドバイスでも大歓迎です！

Java API を使用して Z3 を学習しようとしています。ドキュメントがないため、C API ドキュメントを見てきましたが、基本的な関数の使用方法の明確な例が今まで見つかりませんでした。

この Z3 コードをエンコードしようとしています (オンライン バージョンで動作します)。

今までは、解釈されていないソートを宣言し、関数を次のように宣言するだけでした

しかし、表現する例が見つかりません

誰かがこれで私を助けてくれますか? この asserts-foralls を Java API で表現する方法はどれですか?