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

VPDomain/array equality domain: arrays as values #224

Closed
alexandernutz opened this issue Sep 12, 2017 · 0 comments
Closed

VPDomain/array equality domain: arrays as values #224

alexandernutz opened this issue Sep 12, 2017 · 0 comments
Assignees

Comments

@alexandernutz
Copy link
Member

so far we had a strict separation between arrays and values/nodes/elements

We had a special case for multidimensional arrays.

We want to support the more general case where arrays can be elements, too.

For example if a is a two-dimensional array, a[i] has both aspects: it is a value in a, but it is also a one-dimensional array.

steps on the way:

  • should obsolete any occurence of the MultiDimensionalStore wrapper class
  • adapt the TransFormula to EqConstraint conversion
  • rework the congruence closure class to remove the strict separation between function and element
  • implement the more general propagation rules
@alexandernutz alexandernutz self-assigned this Sep 12, 2017
alexandernutz added a commit that referenced this issue Sep 12, 2017
…o replaces nested stores at the value position, #224
alexandernutz added a commit that referenced this issue Sep 13, 2017
…ICongruenceClosureElement now has a method isFunction() instead.

This is needed because functions (or arrays) may also be arguments to functions. #224
alexandernutz added a commit that referenced this issue Sep 13, 2017
alexandernutz added a commit that referenced this issue Sep 14, 2017
alexandernutz added a commit that referenced this issue Sep 15, 2017
alexandernutz added a commit that referenced this issue Sep 15, 2017
alexandernutz added a commit that referenced this issue Sep 18, 2017
…he arrays/functions are in the first argument position, same otherwise -- towards #224 done right
alexandernutz added a commit that referenced this issue Sep 18, 2017
…nly fail because of lack of precision, roughly, #224
alexandernutz added a commit that referenced this issue Sep 21, 2017
alexandernutz added a commit that referenced this issue Sep 21, 2017
alexandernutz added a commit that referenced this issue Sep 21, 2017
 - untangle WeqCongruenceClosure.reportEquality and CongruenceClosure.reportEquality such that the above can be called right after a merge, and sanityChecks are possible
#224
alexandernutz added a commit that referenced this issue Sep 21, 2017
alexandernutz added a commit that referenced this issue Sep 23, 2017
…o retain information that would otherwise be lost through the remove, (was only done in WeqCongruenceClosure before..)

also: fixes to bwcc propagation
 #224
alexandernutz added a commit that referenced this issue Sep 25, 2017
 - floyd warshall and propagation of array equalites from weq graph are done more often
#224
alexandernutz added a commit that referenced this issue Sep 25, 2017
alexandernutz added a commit that referenced this issue Sep 25, 2017
…nly look for nodes that can be constrained through weak equivalences, as the strong ones are handled in CongruenceClosure now (since a few commits before..), #224
alexandernutz added a commit that referenced this issue Sep 26, 2017
…sults), was in WeakEquivalenceGraph.projectElement, some streamlining, #224
alexandernutz added a commit that referenced this issue Sep 28, 2017
…ruenceClosure (best effort), tried to keep as many sanity checks as possible, #224
alexandernutz added a commit that referenced this issue Sep 28, 2017
…tly got "true" as the new edgeLabel because we were not looking for subnodes with weq-variables, #224
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

No branches or pull requests

1 participant