1

TL;DR: を使用すると、ビット ベクトル除算ノードが からにZ3_OP_BSDIV変わります。除算操作と未解釈の操作をどのように区別できますか?Z3_OP_UNINTERPRETEDsimplify

説明：

次のセッションは、ビット ベクトル除算が解釈されることを示していますが、 を使用した後は解釈されませんsimplify()。以下の変数で何が起こるかを見てくださいd。

>>> x, y = BitVecs('x y', 32)
>>> n = x/y
>>> n.decl().kind()
1031L
>>> d = simplify(x/y)
>>> d.decl().kind()
2051L

UDiv手動で宣言された未解釈の関数があり、同じ種類もあることがわかります。

>>> foo = Function('foo', BitVecSort(32), BitVecSort(32), BitVecSort(32))
>>> u = foo(x, y)
>>> u.decl().kind()
2051L
>>> d1 = simplify(UDiv(x,y))
>>> d1.decl().kind()
2051L

ただし、解法には影響していないようです。ソルバーは依然として演算を実際の除算として解釈しているようです。

>>> prove(d != 400)
counterexample
[y = 1, x = 400]

ノードを種類ごとに処理しようとしていますが、これはその種類について「嘘をついている」ようです。実際に解釈されていることを知る方法はありkindますZ3_OP_UNINTERPRETEDか? これはバグですか？

4

1 に答える 1

1

This is not necessarily a bug. The result of the bvudiv/bvsdiv operators is undefined when the denominator is zero (see QF_BV logic definition). Therefore, the result of "x/y" may be considered undefined and the replacement with an uninterpreted function is warranted if there are no other constraints. Consequently, simplifiers for bit-vector formulas have to take into account that uninterpreted functions may appear in simplified terms.

于 2013-07-15T13:34:54.180 に答える