Z3のビットベクトルをゼロ/符号拡張する方法は？

Question

Z3 SMTインターフェイスを使用してビットベクトルにゼロ拡張を実行できませんでした。ソースを読んで学んだことから、これには関数があり、さまざまなバインディング（C、C++、Pythonなど）で使用できますが、SMTインターフェイスのチュートリアルでは、どのように呼び出すかわかりません。

SMT QF_BVロジック規格のzero_extendを使用すると、Z3はunsupportedと表示されます。

Answer 1

それはzero_extendといくつかの他の機能はパラメトリックもの、Cでfoo<T>のようなおそらく何か++あることが判明しました。特別な構文を使用する1つの必要な関数を呼び出すには：代わりに(zero_extend i x)の((_ zero_extend i) x)を使用して

(declare-const a (_ BitVec 1)) 
(declare-const b (_ BitVec 2)) 
(assert (= b ((_ zero_extend 1) a))) 
(check-sat) 
(get-model) 

は、正しい結果を与える：

sat 
(model 
    (define-fun a() (_ BitVec 1) #b0) 
    (define-fun b() (_ BitVec 2) #b00) 
)