search

OCamlPro / alt-ergo

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

feat(BV): Support binary distinct on arbitrary bit-widths #1222

Closed bclement-ocp closed 2 weeks ago

bclement-ocp commented 2 weeks ago

This used to be impossible to do in the general case when we have only bitlist domains, but is possible since we also have interval domains.

This implementation only supports binary distinct operators, and will need to be revisited as part of #1157.

Note: this currently raises an Internal_error with --enable-assertions due to cross-propagation not running to completion. #1221 fixes this error.

bclement-ocp commented 2 weeks ago

Rebased after the merge of #1221 CI should succeed now.

Halbaroth commented 2 weeks ago

Did you run benchmarks to ensure there is slow down? If our implementation of cross-propagation is correct, we shouldn't raise an error but we could run this PR with --enable-assertions to check if we can catch such a mistake with this test.

bclement-ocp commented 2 weeks ago

Interesting, this seems to break optim-4.models.smt2? Looking into it

bclement-ocp commented 2 weeks ago

Interesting, this seems to break optim-4.models.smt2? Looking into it

This looks like a bug in the optimization procedure that was revealed by this change.