問題タブ [z3py]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
z3 - Z3 から最終的な CNF 式を取得できますか?
これが私の単純なエンコーディングです。これらすべての制約を提示する最終的なブール CNF を取得したいと思います。最終的なブール CNF を取得するための Z3 ソルバーのオプションはありますか?
ありがとうございます。それでは、お元気で
z3 - Z3 の Python API を使用して量指定子の削除を行う方法
Z3 の Python API を使用して量指定子の削除を実行するにはどうすればよいですか? チュートリアルとAPIを確認しましたが、どうにかできませんでした。
存在量指定子を含む式があり、この量指定子が削除されるように、Z3 に新しい式を提供してもらいたいです。私は本質的にこれと同じことをしたい:
ただし、Python インターフェイスを使用します。また、私の式は線形演算です。
ありがとう！
追加: 量指定子の削除を行った後、量指定子のない式を別の式に「追加」します。したがって、戦術を利用する場合、サブゴール (戦術の出力) を線形演算の式に変換する方法はありますか?
z3 - Z3Py を使用して量指定子の除去を実行する方法と、電気ネットワークの場合の Taylor のアイデア
次の電気回路網を考慮してください
この電気回路網の SAT 問題は
この問題は、次のコードを使用してオンラインで Z3Py を使用して解決されます。
出力は次のとおりです。
最後に、Z3Py を使用して、量指定子除去の線形問題を解決します。
対応する出力は次のとおりです。
ここでこの例をオンラインで実行します
線形の例で Z3Py が量指定子の除去を完全に実行しない理由を教えてください。Z3Pyオンラインを使用して、量指定子の除去の元の非線形問題を解決できた場合。どうもありがとう。
z3 - 配列を含むブール式を評価するように Z3 モデルを強制することは可能ですか?
モデルでブール式を評価しても、式に具体的な値が明確に含まれている場合でも、具体的なブール値が返されないことがあります。これを、このテスト ケースのような配列式を含むケースに減らすことができました。
これが印刷されることを期待しますFalseが、代わりに印刷されK(Int, 0) == Store(K(Int, 0), 0, 1)ます。他の例でも同様の結果が得られます。最初の行を に置き換えてx = Array('x', IntSort(), IntSort())も、同じ結果が得られます (ただし、それはデフォルトの解釈次第です)。興味深いことに、最初の行を に置き換えるx = Store(K(IntSort(), 0), 0, 1)と、例が出力されますTrue。
Z3にそのような式を具体的な値に評価させる方法はありますか?
z3 - 数値引数付きの * が単純化によって平坦化されないのはなぜですか?
simplifyと:flat評価さ3 * x * y * zれると予想され(* 3 x y z)ます。代わりに、結果は(* 3 (* x y z))です。なんで？
例
z3 - push コマンドを使用した Z3 でのインクリメンタル ソルビング
Z3 の python API を使用して、ある種のインクリメンタル ソリューションを実行しています。コマンドを使用して、各ステップで満たされないかどうかをチェックしながら、繰り返しソルバーに制約をプッシュしますsolver.push()。Z3 が以前の制約から学習した補題を使用するのか、それとも新しく追加された制約で解くときに以前に得られた満足のいく解を使用するのかを理解したいと思います。私は決してsolver.pop()コマンドを使用しません。以前の反復で行われた作業がどのように使用されているかについての詳細はどこで入手できますか?