z3 - ビット ベクトルを符号付き 10 進数としてきれいに印刷するオプションはありますか?

Question

Z3 でビット ベクトルを符号付き 10 進数としてきれいに印刷するにはどうすればよいですか?

Answer 1

このコマンド(set-option :pp-bv-literals false)を使用して、Z3 にビットベクトル リテラルを 10 進数ベースの形式で表示させることができます。実際には、SMT 2.0 形式を使用して表示されます: (_ bv<decimal> <size>). 次の例を検討してください。

(simplify #x00f8)
(set-option :pp-bv-literals false)
(simplify #x00f8)

Z3が印刷します

#x00f8
(_ bv248 16)

Z3 は符号付き 10 進数をサポートしていません。の最上位ビットが 1 であるかのようにビット ベクトルnを表示するオプションを追加できます。これで十分ですか?(bvneg (_ bv<decimal> <size>)n