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

Rearrangement in Congruence Closure #138

Closed
DavePearce opened this Issue Oct 8, 2017 · 1 comment

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented Oct 8, 2017

The following fails to verify:

assert "negative length possible":
    forall(int n, int[] a):
        if:
            |a| == n
        then:
            n >= 0

The generated proof is this:

 35. exists(int n, int[] a).((((|a| == n)) && ((0 >= (n + 1)))))             () 
 40. exists(int n, int[] a).((n == |a|) && (0 >= (1 + n)))            (Simp 35) 
 39. (n == |a|) && (0 >= (1 + n))                                 (Exists-E 40) 
 36. n == |a|                                                        (And-E 39) 
 38. 0 >= (1 + n)                                                    (And-E 39) 

In contrast, this minor variation does verify:

assert "negative length possible":
    forall(int n, int[] a):
        if:
            n == |a|
        then:
            n >= 0

And the generated proof is:

 35. exists(int n, int[] a).((((n == |a|)) && ((0 >= (n + 1)))))             () 
 39. exists(int n, int[] a).((n == |a|) && (0 >= (1 + n)))            (Simp 35) 
 38. (n == |a|) && (0 >= (1 + n))                                 (Exists-E 39) 
 25. n == |a|                                                        (And-E 38) 
 37. 0 >= (1 + n)                                                    (And-E 38) 
 41. 0 >= (1 + |a|)                                                (Eq-S 37,25) 
 42. |a| >= 0                                                     (ArrLen-I 41) 
 24. false                                                        (Ieq-I 42,41) 

It's pretty odd that, given apparently the same initial state, we end up with a different outcome. The key issue revolves around the method CongruenceClosure.rearrangeToAssignment. In the first case, this gives:

REARRANGED: |a| := n

In the second case, this gives:

REARRANGED: n := |a|

This definitely explains the difference.

@DavePearce

This comment has been minimized.

Member

DavePearce commented Oct 8, 2017

UPDATE: the essential problem comes down to this function:

private static boolean lessThan(Expr lhs, Expr rhs) {
    return lhs.getIndex() < rhs.getIndex();
}

It chooses whichever variable access expression comes first. This doesn't seem optimal!!

DavePearce added a commit that referenced this issue Oct 9, 2017

Fix for congruence rearrangement #138
This implements an interesting fix for congruence rearrangement which
stops using just the heap index, and does a more detailed analysis of
expression in order to choose the equivalence class representative.

@DavePearce DavePearce closed this Oct 9, 2017

DavePearce added a commit that referenced this issue Oct 13, 2017

Fix for congruence closure #138
The fix for Issue 138 was not completely right.  In essence, it
implemented its own compareTo method.  However, it should have been just
using the compareTo method already provided on AbtstractSyntacticItem.
This would then have made it consistent with simplification.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment