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

Fix issue 929 #1209

Draft
wants to merge 2 commits into
base: next
Choose a base branch
from
Draft

Fix issue 929 #1209

wants to merge 2 commits into from

Commits on Aug 14, 2024

  1. Fix issue 929 

    This PR fixes the issue OCamlPro#929 about model arrays.
Our implementation of `ArrayEx` is complete but we do not split on
literals `a = b` where `a` and `b` are any arrays of the problem. Doing
these splits during the search proof would be a bad idea because we do
not need them to be complete. In the example of the issue OCamlPro#929, we
obtain an equality of the form `(store a1 x y) = (store a2 x y)` and
we know that `(select a1 x) = (select a2 x)`. We never try to decide `a1
= a2`.

Notice that I update the set of arrays by tracking literals `Eq` of
origin `Subst`. We know that this design is fragile because it could
happen that substitutions are not sent to theories. The worst that can
happen is to produced wrong models for arrays in very tricky cases.
A better implementation consists in using our new global domains system to
track `selects` in `Adt_rel` and use the keys of this map instead of
`arrays`. I did not opt to this implementation to keep this PR simple
and atomic.
    @Halbaroth
    Halbaroth committed Aug 14, 2024
    Configuration menu
    Copy the full SHA
    1026747 View commit details
    Browse the repository at this point in the history

  2. linter

    @Halbaroth
    Halbaroth committed Aug 14, 2024
    Configuration menu
    Copy the full SHA
    106e60f View commit details
    Browse the repository at this point in the history