search

boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
506 stars 111 forks source link

Optimize blocks #919

Closed keyboardDrummer closed 1 month ago

keyboardDrummer commented 2 months ago

Changes

  1. Perform block coalescing for each split
  2. Add a post-split simplification that removes empty blocks with at most one outgoing or incoming edge

Testing

shazqadeer commented 2 months ago

The block coalescing feature already exists in Boogie and appears to be on by default:

https://github.com/boogie-org/boogie/blob/1b8d9637600e5e0c6fd59e5a760f323c5380ed13/Source/ExecutionEngine/CommandLineOptions.cs#L1900

keyboardDrummer commented 2 months ago

The block coalescing feature already exists in Boogie and appears to be on by default:

https://github.com/boogie-org/boogie/blob/1b8d9637600e5e0c6fd59e5a760f323c5380ed13/Source/ExecutionEngine/CommandLineOptions.cs#L1900

Thanks. The coalescing I'm running happens for each split, after other optimizations which may enable more coalescing, so there is benefit in doing it again.

However, I've removed the duplicate coalescing implementation that this PR adds.