Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Associate syntactic terms to bitvector variables #685

Merged
merged 3 commits into from
Jun 23, 2023

Conversation

bclement-ocp
Copy link
Collaborator

This is a new version of #679, which itself was a new version of #472. A similar fix is also in #553 as bb55438

The crux of it is that the bitvector theory returns interpreted values as leaves, where the rest of the solver requires leaves to be uninterpreted terms.

The main difference of this patch with the other patches above is that here we only create the fresh terms associated with variables after solving, so we only create fresh terms that we do expose. On the other hand, the solver may create many variables internally that gets split or otherwise merged and whose associated terms would never get used.

Fixes #350
Fixes #664

This is a new version of OCamlPro#679, which itself was a new version of OCamlPro#472.
A similar fix is also in OCamlPro#553 as bb55438

The crux of it is that the bitvector theory returns *interpreted* values
as leaves, where the rest of the solver requires leaves to be
*uninterpreted terms*.

The main difference of this patch with the other patches above is that
here we only create the fresh terms associated with variables *after*
solving, so we only create fresh terms that we do expose. On the other
hand, the solver may create many variables internally that gets split or
otherwise merged and whose associated terms would never get used.

Fixes OCamlPro#350
Fixes OCamlPro#664
Copy link
Contributor

@hra687261 hra687261 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

src/lib/reasoners/bitv.ml Show resolved Hide resolved
src/lib/reasoners/bitv.ml Show resolved Hide resolved
src/lib/reasoners/bitv.ml Outdated Show resolved Hide resolved
tests/issues/350.ae Outdated Show resolved Hide resolved
@bclement-ocp bclement-ocp enabled auto-merge (squash) June 23, 2023 10:28
@bclement-ocp bclement-ocp merged commit 6046928 into OCamlPro:next Jun 23, 2023
@bclement-ocp bclement-ocp deleted the bclement/syntbiv branch January 3, 2024 14:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Unsoundness with bit-vectors. [Bug] Assertion failure in lib/reasoners/shostak.ml when reasoning on bitv
2 participants