Replies: 1 comment 4 replies
-
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. |
Beta Was this translation helpful? Give feedback.
4 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
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 assertionx < y
, in whichy
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, sincez3.If(100 + x <= 200000000, 0, 123
cannot automatically be simplified to0
. This means that my custom cache cannot be efficiently used, as the values are not properly simplified to what they could beHence, 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)?Beta Was this translation helpful? Give feedback.
All reactions