CODEWITHSUNDEEP
z3divisionz3py
EfForEffort
EfForEffort

Reputation: 55858

In Z3py, why does simplify turn division into an uninterpreted function?

TL;DR: Bit vector division nodes change from Z3_OP_BSDIV to Z3_OP_UNINTERPRETED when using simplify. How can I tell a division operation from uninterpreted ops?

Explanation:

The following session shows that bit vector division is interpreted, but, after using simplify(), it is uninterpreted. See what happens with the variable d below.

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

We can see that a manually declared uninterpreted function and UDiv have the same kind as well.

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

However, it doesn't seem to affect solving: the solver still seems to interpret the operation as actual division.

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

I am trying to process nodes by their kinds, but this one seems to "lie" about its kind -- is there a way to know that it's really interpreted, even though its kind is Z3_OP_UNINTERPRETED? Is this a bug?

Upvotes: 1

Views: 349

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

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.

Upvotes: 1

Related Questions