1
Z3 SMTインターフェイスを使用してビットベクトルにゼロ拡張を実行できませんでした。ソースを読んで学んだことから、これには関数があり、さまざまなバインディング(C、C++、Pythonなど)で使用できますが、SMTインターフェイスのチュートリアルでは、どのように呼び出すかわかりません。Z3のビットベクトルをゼロ/符号拡張する方法は?
SMT QF_BVロジック規格のzero_extend
を使用すると、Z3はunsupported
と表示されます。
絶対に正しいのです。つまり、zero_extendは、(とりわけ)パラメトリックです。私はそれをLatex構文の$ f_i $と考えています。 –