問題タブ [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.
python - 行列を定義する方法は?
Microsoft が "rise4fun" Web サイトを完全に盗み、Z3 Python チュートリアルが読み込まれなくなったようです。
Z3 for Python で行列を定義し、それにいくつかの制約を課すにはどうすればよいですか?
z3 - z3pyでコア数を設定するにはどうすればよいですか
http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.htmlによると、.smt ファイルを使用している場合、z3 コマンド ラインから CC_NUM_THREADS=4 を設定できます。
z3py API を使用している場合、これを行うにはどうすればよいですか?
python - またはz3Pyのビットベクトルの
理想的には、ビットベクトルとして表される 2 つの数値を「論理和」することが可能ですが、私にはできません。コードにエラーがあるかどうか教えてください。
与えられたエラーは
このエラーから、Or は bool 変数に対してのみ実行できることがわかりました。私の質問は、または BitVectors の方法です
python - z3またはz3pyで絶対値を計算する方法
いくつかの項の絶対値を含む小さな問題を解決しようとしています。z3 では、abs() 関数はサポートされていません。Pythonにはありますが、最終的にはz3pyに渡す必要があります。Pythonからz3に絶対演算子を使用して用語を渡す方法はありますか、それとも他の方法はありますか? 以下は、小さな例のコードです。
abs() を削除した場合、答えは y=1 になるはずです。この問題を絶対値関数で解決する方法はありますか? abs()。または、Pythonで解決してz3に渡す方法はありますか。sympy も試しましたが、うまくいきません。
function - 定義済みの Python 関数を Z3py で動作させるにはどうすればよいですか?
Z3 の初心者として、定義済みの Python 関数で Z3Py を動作させる方法があるかどうか疑問に思っています。以下は、私の質問を説明する小さな例です。
f(x) は Python で定義されている関数です。x <= 0 の場合、f(x) は 0 を返します。制約を追加し、 s.insert(f(a) == 0)Z3 が変数 "a" の適切な値 (たとえば -3) を見つけられることを期待します。しかし、これらのコードは正しく機能していません。どのように変更すればよいですか？
(Z3 の外部で定義された f(x) が必要であり、Z3 によって呼び出されることに注意してください。)
私がやろうとしているのは、Z3 に変換せずに、グラフ ライブラリによって提供される事前定義された関数を呼び出すことです。私はNetworkXライブラリを使用しています.いくつかのコードは次のように与えられています:
この頂点を削除した後、G2 が G1 と同型になるように、G2 の頂点を見つけるのに Z3 が必要です。例えば
python - 反復による最適化
こんにちは、非常に基本的な反復プロセスを通じて、いくつかの制約がある目的関数の最小値を見つけようとしています。問題は、浮動小数点の問題が原因でプログラムが終了しないことです。10 進数で 15 桁までの精度が必要ですが、z3 または python でその精度を超える値を調査する必要はありません。コードは次のとおりです。Mathematica で計算した正確な結果は、a=1、b=2、c=3、d=4、e=5、f=6 であり、対応する目的関数の最小値は 2.06846* です。 10^-14。同じ結果を計算できる可能性はありますか？
コードは次のとおりです: (式が非常に長いため、コピーして貼り付けて実行してください)