search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

SimpleNodeEliminator: Allow restricted elimination of nodes with hyperedges #43

Closed blishko closed 11 months ago

blishko commented 1 year ago

This change extends SimpleNodeEliminator so it also eliminates nodes with single incoming simple edge and any number of outgoing (hyper)edges. Previously, a node was not eliminated if it participated in a hyperedge.

The proposed change leads to more nodes eliminated in some benchmarks of CHC-COMP, which helps the Spacer engine on nonlinear systems. Additionally, some nonlinear systems can be translated to linear ones by this transformation, enabling other engines to solve some nonlinear benchmarks.

blishko commented 1 year ago

comparison

Comparison on CHC-COMP 22 selection shows nice speedup in many benchmarks. There are some safe benchmarks which were not solved in the new version. This would be good to investigate. But overall, this change has benefits that outweigh the lost of these few benchmarks.