Does an alternative to loop unrolling exist?

TikhonJelvis / imp

Some scripts for analyzing IMP programs with the Z3 automatic theorem prover, originally written for my Compose 2016 talk.

http://jelv.is/talks/compose-2016

BSD 3-Clause "New" or "Revised" License

16 stars 1 forks source link

Does an alternative to loop unrolling exist? #3

Open void4 opened 5 months ago

void4 commented 5 months ago

I'm not sure if this is how it actually works, but if all loops are unrolled immediately \<bound>-number of times then the problems become pretty huge. Are there alternatives that can lazily unroll while Z3 is attempting to solve the system? Or perhaps (hybrid) symbolic approaches?