Skip to content

Commit a808179

Browse files
rcosta358rcosta358
committed
Add Tests
1 parent b9a3513 commit a808179

File tree

1 file changed

+190
-0
lines changed

1 file changed

+190
-0
lines changed

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

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -550,6 +550,196 @@ void testTransitive() {
550550
assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1");
551551
}
552552

553+
@Test
554+
void testVarToVarPropagationWithInternalVariable() {
555+
// Given: #x_0 == a && #x_0 > 5
556+
// Expected: a > 5 (internal #x_0 substituted with user-facing a)
557+
558+
Expression varX0 = new Var("#x_0");
559+
Expression varA = new Var("a");
560+
Expression x0EqualsA = new BinaryExpression(varX0, "==", varA);
561+
Expression x0Greater5 = new BinaryExpression(varX0, ">", new LiteralInt(5));
562+
Expression fullExpression = new BinaryExpression(x0EqualsA, "&&", x0Greater5);
563+
564+
// When
565+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
566+
567+
// Then
568+
assertNotNull(result, "Result should not be null");
569+
assertEquals("a > 5", result.getValue().toString(),
570+
"Internal variable #x_0 should be substituted with user-facing variable a");
571+
}
572+
573+
@Test
574+
void testVarToVarInternalToInternal() {
575+
// Given: #a_1 == #b_2 && #b_2 == 5 && x == #a_1 + 1
576+
// Expected: x == 5 + 1 = x == 6
577+
578+
Expression varA = new Var("#a_1");
579+
Expression varB = new Var("#b_2");
580+
Expression varX = new Var("x");
581+
Expression five = new LiteralInt(5);
582+
Expression aEqualsB = new BinaryExpression(varA, "==", varB);
583+
Expression bEquals5 = new BinaryExpression(varB, "==", five);
584+
Expression aPlus1 = new BinaryExpression(varA, "+", new LiteralInt(1));
585+
Expression xEqualsAPlus1 = new BinaryExpression(varX, "==", aPlus1);
586+
Expression firstAnd = new BinaryExpression(aEqualsB, "&&", bEquals5);
587+
Expression fullExpression = new BinaryExpression(firstAnd, "&&", xEqualsAPlus1);
588+
589+
// When
590+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
591+
592+
// Then
593+
assertNotNull(result, "Result should not be null");
594+
assertEquals("x == 6", result.getValue().toString(),
595+
"#a should resolve through #b to 5 across passes, then x == 5 + 1 = x == 6");
596+
}
597+
598+
@Test
599+
void testVarToVarDoesNotAffectUserFacingVariables() {
600+
// Given: x == y && x > 5
601+
// Expected: x == y && x > 5 (user-facing var-to-var should not be propagated)
602+
603+
Expression varX = new Var("x");
604+
Expression varY = new Var("y");
605+
Expression xEqualsY = new BinaryExpression(varX, "==", varY);
606+
Expression xGreater5 = new BinaryExpression(varX, ">", new LiteralInt(5));
607+
Expression fullExpression = new BinaryExpression(xEqualsY, "&&", xGreater5);
608+
609+
// When
610+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
611+
612+
// Then
613+
assertNotNull(result, "Result should not be null");
614+
assertEquals("x == y && x > 5", result.getValue().toString(),
615+
"User-facing variable equalities should not trigger var-to-var propagation");
616+
}
617+
618+
@Test
619+
void testVarToVarRemovesRedundantEquality() {
620+
// Given: #ret_1 == #b_0 - 100 && #b_0 == b && b >= -128 && b <= 127
621+
// Expected: #ret_1 == b - 100 && b >= -128 && b <= 127 (#b_0 replaced with b, #b_0 == b removed)
622+
623+
Expression ret1 = new Var("#ret_1");
624+
Expression b0 = new Var("#b_0");
625+
Expression b = new Var("b");
626+
Expression ret1EqB0Minus100 = new BinaryExpression(ret1, "==",
627+
new BinaryExpression(b0, "-", new LiteralInt(100)));
628+
Expression b0EqB = new BinaryExpression(b0, "==", b);
629+
Expression bGeMinus128 = new BinaryExpression(b, ">=", new UnaryExpression("-", new LiteralInt(128)));
630+
Expression bLe127 = new BinaryExpression(b, "<=", new LiteralInt(127));
631+
Expression and1 = new BinaryExpression(ret1EqB0Minus100, "&&", b0EqB);
632+
Expression and2 = new BinaryExpression(bGeMinus128, "&&", bLe127);
633+
Expression fullExpression = new BinaryExpression(and1, "&&", and2);
634+
635+
// When
636+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
637+
638+
// Then
639+
assertNotNull(result, "Result should not be null");
640+
assertEquals("#ret_1 == b - 100 && b >= -128 && b <= 127", result.getValue().toString(),
641+
"Internal variable #b_0 should be replaced with b and redundant equality removed");
642+
assertNotNull(result.getOrigin(), "Origin should be present showing the var-to-var derivation");
643+
}
644+
645+
@Test
646+
void testInternalToInternalReducesRedundantVariable() {
647+
// Given: #a_3 == #b_7 && #a_3 > 5
648+
// Expected: #b_7 > 5 (#a_3 has lower counter, so #a_3 -> #b_7)
649+
650+
Expression a3 = new Var("#a_3");
651+
Expression b7 = new Var("#b_7");
652+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
653+
Expression a3Greater5 = new BinaryExpression(a3, ">", new LiteralInt(5));
654+
Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", a3Greater5);
655+
656+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
657+
658+
assertNotNull(result);
659+
assertEquals("#b_7 > 5", result.getValue().toString(),
660+
"#a_3 (lower counter) should be substituted with #b_7 (higher counter)");
661+
}
662+
663+
@Test
664+
void testInternalToInternalChainWithUserFacingVariableUserFacingFirst() {
665+
// Given: #b_7 == x && #a_3 == #b_7 && x > 0
666+
// Expected: x > 0 (#b_7 -> x (user-facing); #a_3 has lower counter so #a_3 -> #b_7)
667+
668+
Expression a3 = new Var("#a_3");
669+
Expression b7 = new Var("#b_7");
670+
Expression x = new Var("x");
671+
Expression b7EqualsX = new BinaryExpression(b7, "==", x);
672+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
673+
Expression xGreater0 = new BinaryExpression(x, ">", new LiteralInt(0));
674+
Expression and1 = new BinaryExpression(b7EqualsX, "&&", a3EqualsB7);
675+
Expression fullExpression = new BinaryExpression(and1, "&&", xGreater0);
676+
677+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
678+
679+
assertNotNull(result);
680+
assertEquals("x > 0", result.getValue().toString(),
681+
"Both internal variables should be eliminated via chain resolution");
682+
}
683+
684+
@Test
685+
void testInternalToInternalChainWithUserFacingVariableInternalFirst() {
686+
// Given: #a_3 == #b_7 && #b_7 == x && x > 0
687+
// Expected: x > 0 (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> x (user-facing) overwrites)
688+
689+
Expression a3 = new Var("#a_3");
690+
Expression b7 = new Var("#b_7");
691+
Expression x = new Var("x");
692+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
693+
Expression b7EqualsX = new BinaryExpression(b7, "==", x);
694+
Expression xGreater0 = new BinaryExpression(x, ">", new LiteralInt(0));
695+
Expression and1 = new BinaryExpression(a3EqualsB7, "&&", b7EqualsX);
696+
Expression fullExpression = new BinaryExpression(and1, "&&", xGreater0);
697+
698+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
699+
700+
assertNotNull(result);
701+
assertEquals("x > 0", result.getValue().toString(),
702+
"Both internal variables should be eliminated via fixed-point iteration");
703+
}
704+
705+
@Test
706+
void testInternalToInternalBothResolvingToLiteral() {
707+
// Given: #a_3 == #b_7 && #b_7 == 5
708+
// Expected: 5 == 5 && 5 == 5 -> true (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> 5)
709+
710+
Expression a3 = new Var("#a_3");
711+
Expression b7 = new Var("#b_7");
712+
Expression five = new LiteralInt(5);
713+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
714+
Expression b7Equals5 = new BinaryExpression(b7, "==", five);
715+
Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", b7Equals5);
716+
717+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
718+
719+
assertNotNull(result);
720+
assertEquals("true", result.getValue().toString(),
721+
"#a_3 -> #b_7 -> 5 and #b_7 -> 5; both equalities collapse to 5 == 5 -> true");
722+
}
723+
724+
@Test
725+
void testInternalToInternalNoFurtherResolution() {
726+
// Given: #a_3 == #b_7 && #b_7 + 1 > 0
727+
// Expected: #b_7 + 1 > 0 (#a_3 has lower counter, so #a_3 -> #b_7)
728+
729+
Expression a3 = new Var("#a_3");
730+
Expression b7 = new Var("#b_7");
731+
Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7);
732+
Expression b7Plus1 = new BinaryExpression(b7, "+", new LiteralInt(1));
733+
Expression b7Plus1Greater0 = new BinaryExpression(b7Plus1, ">", new LiteralInt(0));
734+
Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", b7Plus1Greater0);
735+
736+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
737+
738+
assertNotNull(result);
739+
assertEquals("#b_7 + 1 > 0", result.getValue().toString(),
740+
"#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial");
741+
}
742+
553743
/**
554744
* Helper method to compare two derivation nodes recursively
555745
*/

0 commit comments

Comments
 (0)