3

:変数 x は (declare-const x Int) による int ソートとして定義されます

x をビットベクトルソートに変換する方法はありますか? x には、int 理論では処理できない &、|、^ などのビット操作が含まれることがあるためです。

最初に変数 x をビットベクトルとして定義したくありません。なぜなら、ビット演算を除く int 理論でサポートされている演算 (+、-、​​、/ など) は、ビットベクトルでサポートされている演算よりもはるかに高速に実行されると思われるからです。

実際には、必要に応じて int ソートを bitvector ソートまたは vise vesa に変換したいと考えています。

ありがとう。

ティン・チェン

4

1 に答える 1

4

bv2intはい、や などを使用できますint2bv。ビットベクトルの長さが重要であり、int2bv がパラメトリックであることに注意してください (ビットベクトルの長さが必要です)。

最小限の例を次に示します (rise4fun リンク: http://rise4fun.com/Z3/wxcp ):

(declare-fun x () (_ BitVec 32))
(declare-fun y () Int)
(declare-fun z () (_ BitVec 16))
(assert (= y 129))
(assert (= (bv2int x) y))
; (assert (= ((_ int2bv 32) y) x)) ; try with this uncommented
(assert (= ((_ int2bv 16) y) z))
(check-sat)
(get-model)
(get-value (x y z)) ; gives ((x #x00000000) (y 129) (z #x0081))

別の例を次に示します。

Z3: int2bv の例外

現在、これらの関数にいくつかの問題があるようです: Z3 でオーバーフローを確認してください

bv2natこれらは、他のソルバー (および)では異なる名前で呼び出される場合もありますnat2bv: http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2

于 2014-12-03T15:27:37.843 に答える