- User Since
- Dec 15 2016, 10:51 AM (354 w, 6 d)
Aug 12 2019
Seems like a great idea!
May 7 2019
I'm not convinced by the approach.
Feb 4 2019
Nov 30 2018
We indeed have a user of Z3 for LLVM coming soon. (it is not upstreamed yet because the binding with Z3 was botched, it would never have been accepted)
To spill the beans: we wrote a more aggressive SCEV Canonicalizer, as a support class. It does not rely on Z3 to perform the transformation itself, but it uses Z3 into the verifier. (mostly to find potential mistakes, but we could use it to find missed opportunities too)
Nov 28 2018
Great! I have some use cases for verifiers, and in general for research purposes it can be quite useful.
Jun 20 2018
That might be related, for instance, such expressions:
Jun 19 2018
Ah, you are right, I misinterpreted the purpose.
I have been working on related issue but my strategy is different:
Mar 7 2018
Fixed RUN_ON macro typo
Aug 28 2017
Hello, is there any modifications I didn't apply or do you have any change you would like to see?
Aug 16 2017
Updated the test cases and simplified the power-of-two special case.
Aug 15 2017
Please check I didn't introduce new errors (off by one?).
I added handling for urem by a power-of-two so as to fix the failing test-case.
Jun 28 2017
Fixed the short-circuit. (should be 0, not x)
Updated testcase, outlined into a getURemExpr and added a x urem 1 shortcut.
Added an additional testcase with a loop.