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.

Sign up for GitHub

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

Jump to bottom

Missing Subst equalities #883

Closed
bclement-ocp opened this issue Oct 13, 2023 · 0 comments · Fixed by #886
Closed

Missing Subst equalities #883

bclement-ocp opened this issue Oct 13, 2023 · 0 comments · Fixed by #886
Assignees
@bclement-ocp

Comments

@bclement-ocp
Copy link
Collaborator

Contrary to what I claimed in #869 Other equalities are not necessarily subsumed by Subst equalities.

To be more precise, they absolutely are subsumed by Subst equalities, but those Subst then get filtered out in make_unique in Ccx. I know I have a patch lying around for this somewhere that I would have sworn was merged already, I will dig it out.

See for instance:

(set-logic ALL)
(declare-const x Int)
(assert (= ((_ int2bv 2) x) #b11))
(assert (<= x 0))
(assert (<= 0 x))
(check-sat)

which returns unsat because we don't trigger the computation of ((_ int2bv 2) x) even though we learn x = 0.
@bclement-ocp bclement-ocp self-assigned this Oct 13, 2023
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Oct 13, 2023
@bclement-ocp
Preserve Subst literals
e76c1cc 
If we propagate the same literal with multiple origins in a single CC(X)
step (i.e. they end up in the same fact list), we only keep one. We must
make sure to keep the one with `Subst` origin, because those are used by
the union-find communicate with the relations about representative
changes.

Fixes OCamlPro#883
@bclement-ocp bclement-ocp mentioned this issue Oct 13, 2023
Merged
bclement-ocp added a commit that referenced this issue Oct 19, 2023
@bclement-ocp
Preserve Subst literals (#886)
dcb94b0 
If we propagate the same literal with multiple origins in a single CC(X)
step (i.e. they end up in the same fact list), we only keep one. We must
make sure to keep the one with `Subst` origin, because those are used by
the union-find communicate with the relations about representative
changes.

Fixes #883
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bclement-ocp bclement-ocp

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Preserve Subst literals bclement-ocp/alt-ergo
1 participant
@bclement-ocp