0

次の python コードを使用して、次の 2 つの 2 進数を見つけています。

  • 合計して特定の数にする
  • 整数にキャストされた最上位ビットの合計は 2 になる必要があります

2 番目の制約は、私にとってより重要です。私の場合、それはスケーリングします: [N] 数の最上位ビットを合計すると [M] になる可能性があるとしましょう。

z3 が正しい結果を返さない理由がわかりません。ヒントはありますか？どうもありがとう。

def BV2Int(var):
    return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), var.ctx)

def main():
    s = Solver()
    s.set(':models', True) 
    s.set(':auto-cfgig', False) 
    s.set(':smt.bv.enable_int2bv',True) 

    x = BitVec('x',4)
    y = BitVec('y',4)
    s = Solver()
    s.add(x+y == 16, Extract(3,3,x) + Extract(3,3,y) == 2)
    s.check()
    print s.model()
    # result: [y = 0, x = 0], fail both constraint

    s = Solver()
    s.add(x+y == 16, BV2Int(Extract(3,3,x)) + BV2Int(Extract(3,3,y)) == 2)
    s.check()
    print s.model()
    # result: [y = 15, x = 1], fail the second constraint

更新: Christoph からの回答に感謝します。ここに簡単な修正があります：

  • Extract(3,3,x) -> ZeroExt(SZ, Extract(3,3,x)) ここで、SZ は RHS のビット幅から 1 を引いた値です。
4

1 に答える 1

0

(余談: auto-cfgig は auto-config である必要があります。)

bv2int と int2bv は基本的に解釈されないものとして扱われるため、この部分が問題にとって重要な場合は使用しないでください (ドキュメントと以前の質問を参照してください)。

この例の問題は、ビットベクトルの幅です。xとは両方ともy4 ビットの変数であり、164 ビットのベクトルとしての数値は0(modulo 2^4) であるため、確かにwhenとx + yに等しくなります。16x=0y=0

さらに、Extract(...)用語は 1 ビット ベクトルを抽出します。これは、合計Ex.. + Ex..が 1 ビット値であり、21 ビット ベクトルとしての数値が0(モジュロ 2^1) であることを意味しEx... + Ex... = 2ます。

于 2015-08-07T12:05:31.223 に答える