Skip to content

Commit 7e6a7b5

Browse files
rcosta358rcosta358
committed
Substitute Internal Variables by Counter
1 parent 96f7b4c commit 7e6a7b5

3 files changed

Lines changed: 115 additions & 6 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,4 +74,11 @@ public boolean equals(Object obj) {
7474
public boolean isInternal() {
7575
return name.startsWith("#");
7676
}
77+
78+
public int getCounter() {
79+
if (!isInternal())
80+
throw new IllegalStateException("Cannot get counter of non-internal variable");
81+
int lastUnderscore = name.lastIndexOf('_');
82+
return Integer.parseInt(name.substring(lastUnderscore + 1));
83+
}
7784
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,12 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
5858
map.put(leftVar.getName(), right.clone());
5959
} else if (rightVar.isInternal() && !leftVar.isInternal()) {
6060
map.put(rightVar.getName(), left.clone());
61+
} else if (leftVar.isInternal() && rightVar.isInternal()) {
62+
// substitute the lower-counter variable with the higher-counter one
63+
boolean isLeftCounterLower = leftVar.getCounter() <= rightVar.getCounter();
64+
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
65+
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
66+
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
6167
}
6268
}
6369
}

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java‎

Lines changed: 102 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -621,13 +621,11 @@ void testVarToVarPropagationWithInternalVariable() {
621621

622622
@Test
623623
void testVarToVarInternalToInternal() {
624-
// Given: #a == #b && #b == 5 && x == #a + 1
625-
// Internal-to-internal var-to-var is resolved across fixed-point passes:
626-
// Pass 1: #b -> 5 => #a == 5 && x == #a + 1
627-
// Pass 2: #a -> 5 => x == 6
624+
// Given: #a_1 == #b_2 && #b_2 == 5 && x == #a_1 + 1
625+
// Expected: x == 5 + 1 = x == 6
628626

629-
Expression varA = new Var("#a");
630-
Expression varB = new Var("#b");
627+
Expression varA = new Var("#a_1");
628+
Expression varB = new Var("#b_2");
631629
Expression varX = new Var("x");
632630
Expression five = new LiteralInt(5);
633631
Expression aEqualsB = new BinaryExpression(varA, "==", varB);
@@ -693,6 +691,104 @@ void testVarToVarRemovesRedundantEquality() {
693691
assertNotNull(result.getOrigin(), "Origin should be present showing the var-to-var derivation");
694692
}
695693

694+
@Test
695+
void testInternalToInternalReducesRedundantVariable() {
696+
// Given: #a_3 == #b_7 && #a_3 > 5
697+
// Expected: #b_7 > 5 (#a_3 has lower counter, so #a_3 -> #b_7)
698+
699+
Expression a3 = new Var("#a_3");
700+
Expression b7 = new Var("#b_7");
701+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
702+
Expression a3Greater5 = new BinaryExpression(a3, ">", new LiteralInt(5));
703+
Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", a3Greater5);
704+
705+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
706+
707+
assertNotNull(result);
708+
assertEquals("#b_7 > 5", result.getValue().toString(),
709+
"#a_3 (lower counter) should be substituted with #b_7 (higher counter)");
710+
}
711+
712+
@Test
713+
void testInternalToInternalChainWithUserFacingVariableUserFacingFirst() {
714+
// Given: #b_7 == x && #a_3 == #b_7 && x > 0
715+
// Expected: x > 0 (#b_7 -> x (user-facing); #a_3 has lower counter so #a_3 -> #b_7)
716+
717+
Expression a3 = new Var("#a_3");
718+
Expression b7 = new Var("#b_7");
719+
Expression x = new Var("x");
720+
Expression b7EqualsX = new BinaryExpression(b7, "==", x);
721+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
722+
Expression xGreater0 = new BinaryExpression(x, ">", new LiteralInt(0));
723+
Expression and1 = new BinaryExpression(b7EqualsX, "&&", a3EqualsB7);
724+
Expression fullExpression = new BinaryExpression(and1, "&&", xGreater0);
725+
726+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
727+
728+
assertNotNull(result);
729+
assertEquals("x > 0", result.getValue().toString(),
730+
"Both internal variables should be eliminated via chain resolution");
731+
}
732+
733+
@Test
734+
void testInternalToInternalChainWithUserFacingVariableInternalFirst() {
735+
// Given: #a_3 == #b_7 && #b_7 == x && x > 0
736+
// Expected: x > 0 (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> x (user-facing) overwrites)
737+
738+
Expression a3 = new Var("#a_3");
739+
Expression b7 = new Var("#b_7");
740+
Expression x = new Var("x");
741+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
742+
Expression b7EqualsX = new BinaryExpression(b7, "==", x);
743+
Expression xGreater0 = new BinaryExpression(x, ">", new LiteralInt(0));
744+
Expression and1 = new BinaryExpression(a3EqualsB7, "&&", b7EqualsX);
745+
Expression fullExpression = new BinaryExpression(and1, "&&", xGreater0);
746+
747+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
748+
749+
assertNotNull(result);
750+
assertEquals("x > 0", result.getValue().toString(),
751+
"Both internal variables should be eliminated via fixed-point iteration");
752+
}
753+
754+
@Test
755+
void testInternalToInternalBothResolvingToLiteral() {
756+
// Given: #a_3 == #b_7 && #b_7 == 5
757+
// Expected: 5 == 5 && 5 == 5 -> true (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> 5)
758+
759+
Expression a3 = new Var("#a_3");
760+
Expression b7 = new Var("#b_7");
761+
Expression five = new LiteralInt(5);
762+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
763+
Expression b7Equals5 = new BinaryExpression(b7, "==", five);
764+
Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", b7Equals5);
765+
766+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
767+
768+
assertNotNull(result);
769+
assertEquals("true", result.getValue().toString(),
770+
"#a_3 -> #b_7 -> 5 and #b_7 -> 5; both equalities collapse to 5 == 5 -> true");
771+
}
772+
773+
@Test
774+
void testInternalToInternalNoFurtherResolution() {
775+
// Given: #a_3 == #b_7 && #b_7 + 1 > 0
776+
// Expected: #b_7 + 1 > 0 (#a_3 has lower counter, so #a_3 -> #b_7)
777+
778+
Expression a3 = new Var("#a_3");
779+
Expression b7 = new Var("#b_7");
780+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
781+
Expression b7Plus1 = new BinaryExpression(b7, "+", new LiteralInt(1));
782+
Expression b7Plus1Greater0 = new BinaryExpression(b7Plus1, ">", new LiteralInt(0));
783+
Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", b7Plus1Greater0);
784+
785+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
786+
787+
assertNotNull(result);
788+
assertEquals("#b_7 + 1 > 0", result.getValue().toString(),
789+
"#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial");
790+
}
791+
696792
/**
697793
* Helper method to compare two derivation nodes recursively
698794
*/

0 commit comments

Comments
 (0)