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 回答