search

usi-verification-and-security / golem

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

BMC engine is slow compared to Z3 #76

Open blishko opened 1 month ago

blishko commented 1 month ago

On the following benchmark, Golem is much slower than Z3: chc22/LIA-lin/chc-LIA-Lin_442.smt2 It looks like Z3 can successfully simplify the system in preprocessing. We should try to do something similar.

blishko commented 1 month ago

Looks like Z3 is doing some interesting preprocessing where it detects that a recursive clause cannot be taken more than once (because its tail does not unify with its head). Z3 can then resolve this clause and delete it completely, effectively removing one cycle from the graph. We could do something similar, check all the cycles and if we detect that the recursive clause cannot be taken, we can (in the graph terminology) split the vertex into "in" and "out" version, and change the self loop edge into a bridge from "in" to "out".