z3.simplify() with bounds / assertions

[Notselwyn]

Hi, I'm writing a high-performance application. I have a few nifty techniques to save computing time, but I'm noticing that there are a few (very large) computations being thrown into the z3 solver. A lot of them are variations of z3.If(100 + x <= 200000000, 0, 123. However, x has assertion x < y, in which y is a bitvec often less than 500. This value is often a constant value due to the amount of simplification prior to this. Hence, there's a lot of wasted computing power, since z3.If(100 + x <= 200000000, 0, 123 cannot automatically be simplified to 0. This means that my custom cache cannot be efficiently used, as the values are not properly simplified to what they could be

Hence, are there methods to be able to perform these simplifications based on bounds/assertions? I have seen the add-bounds tactic but it seems I cannot utilize the BitVecRef itself for the bounds. Should I do a .as_long()? Or should I use a solver for simplification (if that is even worth it performance-wise)?

[philzook58]

One trick I've used for contextual simplification that I learned from @calebh is to put the assumptions into a Solver or Goal, create a fresh name to the simplified term in an equation, and run a couple tactics (demodulator, elim-predicates, simplify, other useful ones? https://microsoft.github.io/z3guide/docs/strategies/tactics/ ). https://github.com/philzook58/knuckledragger/blob/2f3c04fd11f10c29b91520ad7ae75c3d7efad5db/knuckledragger/utils.py#L9 . You can then root around in the result for the fresh name to get your simplified term. If there is a better way, and there may well be, I'd like to know it.

[Notselwyn]

One trick I've used for contextual simplification that I learned from @calebh is to put the assumptions into a Solver or Goal, create a fresh name to the simplified term in an equation, and run a couple tactics (demodulator, elim-predicates, simplify, other useful ones? https://microsoft.github.io/z3guide/docs/strategies/tactics/ ). https://github.com/philzook58/knuckledragger/blob/2f3c04fd11f10c29b91520ad7ae75c3d7efad5db/knuckledragger/utils.py#L9 . You can then root around in the result for the fresh name to get your simplified term. If there is a better way, and there may well be, I'd like to know it.

Thanks for sending me in the right direction. When I try the following code, I get [i > 2, i < 4], not [i = 3]. Am I misunderstanding your comment?

i = z3.Int('i')
g = z3.Goal()
g.add(i > 2)
g.add(i < 4)
z3.Then('demodulator', 'ctx-simplify').apply(g)[0]

[philzook58]

Your mileage may vary. There's no way you'll catch every possible simplification. https://microsoft.github.io/z3guide/docs/strategies/summary#tactic-propagate-ineqs seems to work for this particular example.

import z3
i = z3.Int('i')
g = z3.Goal()
g.add(i > 2)
g.add(i < 4)
z3.Then('simplify', 'propagate-ineqs').apply(g)
# [[i = 3]]

[Notselwyn]

This is getting close, but I also want to be able to do further operations like x = i + 1, with i.e. i being bounded. Is this possible somehow? I could probably do x = z3.If(i >= 4, 3, z3.If(i <= 2, 3)), but this won't give a sane value for i in the output model

[NikolajBjorner]

if you use the solve-eqs tactic, it will replace either x or i, and the bounds of either are combined.
So propagate-ineqs doesn't attempt to perform double duty of equality inference because this is handled by a different method (solve-eqs).