search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

fix(BV): Internalize sign_extend and repeat #1192

Closed bclement-ocp closed 3 weeks ago

bclement-ocp commented 1 month ago

Currently, we convert sign_extend and repeat to the appropriate concatenations and extractions at the term level. This has the advantage that it is simple, but the inconvenient that we create a potentially large amount of terms that do not appear in the original problem (proportional to the size of the sign extension or repetition).

In addition to preventing obvious simplifications with extractions, the creation of many terms clutters the union-find which drastically slows down the solver in presence of sign extensions to large bit-widths.

Note: this impacts some of the Décysif datasets.

bclement-ocp commented 1 month ago

Note: this impacts some of the Décysif datasets.

More precisely, this patch is on average 6x faster and solves 10% more problems than current next on the J3 dataset.