Skip to content

Commit 1043d1a

Browse files
rcosta358rcosta358
committed
Refactor Tests
1 parent 804c7a6 commit 1043d1a

4 files changed

Lines changed: 115 additions & 102 deletions

File tree

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

Lines changed: 50 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package liquidjava.rj_language.opt;
22

3-
import static liquidjava.utils.VCTestUtils.assertSimplificationSteps;
4-
import static liquidjava.utils.VCTestUtils.vc;
3+
import static liquidjava.utils.VCTestUtils.*;
54
import static org.junit.jupiter.api.Assertions.assertEquals;
65
import static org.junit.jupiter.api.Assertions.assertInstanceOf;
76
import static org.junit.jupiter.api.Assertions.assertNull;
@@ -26,88 +25,98 @@ void applyReturnsNullForNullImplication() {
2625
void foldsIntegerArithmeticAndComparisons() {
2726
VCImplication implication = vc("1 + 2 == 3");
2827

29-
assertSimplificationSteps(VCFolding::apply, implication, "3 == 3", "true");
30-
assertSimplificationSteps(VCFolding::apply, vc("4 > 7"), "false");
28+
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")),
29+
chain(expect("true", "1 + 2 == 3")));
30+
assertSimplificationSteps(VCFolding::apply, vc("4 > 7"), chain(expect("false", "4 > 7")));
3131
}
3232

3333
@Test
3434
void foldsRealAndMixedNumericExpressions() {
3535
VCImplication realArithmetic = vc("1.5 + 2.0 == 3.5");
3636
VCImplication mixedArithmetic = vc("2 + 0.5 > 2");
3737

38-
assertSimplificationSteps(VCFolding::apply, realArithmetic, "3.5 == 3.5", "true");
39-
assertSimplificationSteps(VCFolding::apply, mixedArithmetic, "2.5 > 2", "true");
38+
assertSimplificationSteps(VCFolding::apply, realArithmetic, chain(expect("3.5 == 3.5", "1.5 + 2.0 == 3.5")),
39+
chain(expect("true", "1.5 + 2.0 == 3.5")));
40+
assertSimplificationSteps(VCFolding::apply, mixedArithmetic, chain(expect("2.5 > 2", "2 + 0.5 > 2")),
41+
chain(expect("true", "2 + 0.5 > 2")));
4042
}
4143

4244
@Test
4345
void leavesDivisionAndModuloByZeroUnchanged() {
44-
assertSimplificationSteps(VCFolding::apply, vc("4 / 0 == 0"), "4 / 0 == 0");
45-
assertSimplificationSteps(VCFolding::apply, vc("4 % 0 == 0"), "4 % 0 == 0");
46+
assertSimplificationSteps(VCFolding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0", "4 / 0 == 0")));
47+
assertSimplificationSteps(VCFolding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0", "4 % 0 == 0")));
4648
}
4749

4850
@Test
4951
void leavesRealDivisionAndModuloByZeroUnchanged() {
50-
assertSimplificationSteps(VCFolding::apply, vc("4.0 / 0.0 == 0.0"), "4.0 / 0.0 == 0.0");
51-
assertSimplificationSteps(VCFolding::apply, vc("4.0 % 0.0 == 0.0"), "4.0 % 0.0 == 0.0");
52+
assertSimplificationSteps(VCFolding::apply, vc("4.0 / 0.0 == 0.0"),
53+
chain(expect("4.0 / 0.0 == 0.0", "4.0 / 0.0 == 0.0")));
54+
assertSimplificationSteps(VCFolding::apply, vc("4.0 % 0.0 == 0.0"),
55+
chain(expect("4.0 % 0.0 == 0.0", "4.0 % 0.0 == 0.0")));
5256
}
5357

5458
@Test
5559
void foldsBooleanBinaryExpressions() {
56-
assertSimplificationSteps(VCFolding::apply, vc("true && false"), "false");
57-
assertSimplificationSteps(VCFolding::apply, vc("false --> true"), "true");
58-
assertSimplificationSteps(VCFolding::apply, vc("true != false"), "true");
60+
assertSimplificationSteps(VCFolding::apply, vc("true && false"), chain(expect("false", "true && false")));
61+
assertSimplificationSteps(VCFolding::apply, vc("false --> true"), chain(expect("true", "false --> true")));
62+
assertSimplificationSteps(VCFolding::apply, vc("true != false"), chain(expect("true", "true != false")));
5963
}
6064

6165
@Test
6266
void foldsBooleanSubexpressionsInsideLargerExpression() {
63-
assertSimplificationSteps(VCFolding::apply, vc("true && false || ok"), "false || ok");
67+
assertSimplificationSteps(VCFolding::apply, vc("true && false || ok"),
68+
chain(expect("false || ok", "true && false || ok")));
6469
}
6570

6671
@Test
6772
void foldsNestedConstantsInsideLargerExpression() {
68-
assertSimplificationSteps(VCFolding::apply, vc("x > 1 + 2"), "x > 3");
69-
assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2 > 4"), "x + 3 > 4");
73+
assertSimplificationSteps(VCFolding::apply, vc("x > 1 + 2"), chain(expect("x > 3", "x > 1 + 2")));
74+
assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2 > 4"), chain(expect("x + 3 > 4", "x + 1 + 2 > 4")));
7075
}
7176

7277
@Test
7378
void foldsPartialComparisonsWithoutDroppingSymbolicTerms() {
74-
assertSimplificationSteps(VCFolding::apply, vc("1 + 2 < x + 4"), "3 < x + 4");
79+
assertSimplificationSteps(VCFolding::apply, vc("1 + 2 < x + 4"), chain(expect("3 < x + 4", "1 + 2 < x + 4")));
7580
}
7681

7782
@Test
7883
void foldsUnaryExpressions() {
79-
assertSimplificationSteps(VCFolding::apply, vc("!true"), "false");
84+
assertSimplificationSteps(VCFolding::apply, vc("!true"), chain(expect("false", "!true")));
8085
VCImplication implication = vc("-3 < 0");
8186

82-
assertSimplificationSteps(VCFolding::apply, implication, "-3 < 0", "true");
87+
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("-3 < 0", "-3 < 0")),
88+
chain(expect("true", "-3 < 0")));
8389
}
8490

8591
@Test
8692
void foldsIteExpressions() {
87-
assertSimplificationSteps(VCFolding::apply, vc("true ? a : b"), "a");
88-
assertSimplificationSteps(VCFolding::apply, vc("false ? a : b"), "b");
89-
assertSimplificationSteps(VCFolding::apply, vc("cond ? b : b"), "b");
93+
assertSimplificationSteps(VCFolding::apply, vc("true ? a : b"), chain(expect("a", "true ? a : b")));
94+
assertSimplificationSteps(VCFolding::apply, vc("false ? a : b"), chain(expect("b", "false ? a : b")));
95+
assertSimplificationSteps(VCFolding::apply, vc("cond ? b : b"), chain(expect("b", "cond ? b : b")));
9096
}
9197

9298
@Test
9399
void foldsIteBranchesBeforeComparingThem() {
94100
VCImplication implication = vc("cond ? 1 + 2 : 3");
95101

96-
assertSimplificationSteps(VCFolding::apply, implication, "cond ? 3 : 3", "3");
102+
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("cond ? 3 : 3", "cond ? 1 + 2 : 3")),
103+
chain(expect("3", "cond ? 1 + 2 : 3")));
97104
}
98105

99106
@Test
100107
void foldsAdjacentIntegerConstants() {
101-
assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 2"), "x - 1");
102-
assertSimplificationSteps(VCFolding::apply, vc("x - 1 + 2"), "x + 1");
103-
assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2"), "x + 3");
104-
assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 1"), "x");
108+
assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 2"), chain(expect("x - 1", "x + 1 - 2")));
109+
assertSimplificationSteps(VCFolding::apply, vc("x - 1 + 2"), chain(expect("x + 1", "x - 1 + 2")));
110+
assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2"), chain(expect("x + 3", "x + 1 + 2")));
111+
assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 1"), chain(expect("x", "x + 1 - 1")));
105112
}
106113

107114
@Test
108115
void foldsEnumEqualityAndInequality() {
109-
assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo == Mode.Photo"), "true");
110-
assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo != Mode.Video"), "true");
116+
assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo == Mode.Photo"),
117+
chain(expect("true", "Mode.Photo == Mode.Photo")));
118+
assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo != Mode.Video"),
119+
chain(expect("true", "Mode.Photo != Mode.Video")));
111120
}
112121

113122
@Test
@@ -117,7 +126,8 @@ void foldsResolvedEnumLiterals() {
117126
VCImplication implication = new VCImplication(
118127
new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3))));
119128

120-
assertSimplificationSteps(VCFolding::apply, implication, "3 == 3", "true");
129+
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")),
130+
chain(expect("true", "Config.LIMIT == 3")));
121131
}
122132

123133
@Test
@@ -128,20 +138,23 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() {
128138
VCImplication implication = new VCImplication(
129139
new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5))));
130140

131-
assertSimplificationSteps(VCFolding::apply, implication, "3 + 2 == 5", "5 == 5", "true");
141+
assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 + 2 == 5", "Config.LIMIT + 2 == 5")),
142+
chain(expect("5 == 5", "Config.LIMIT + 2 == 5")), chain(expect("true", "Config.LIMIT + 2 == 5")));
132143
}
133144

134145
@Test
135146
void preservesOriginFromExistingSimplifiedImplication() {
136147
VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0"));
137148

138-
assertSimplificationSteps(VCFolding::apply, substituted, "2 + 2 > 0", "4 > 0", "true");
149+
assertSimplificationSteps(VCFolding::apply, substituted, chain(expect("2 + 2 > 0", "∀x:int. x + 1 + 2 > 0")),
150+
chain(expect("4 > 0", "∀x:int. x + 1 + 2 > 0")), chain(expect("true", "∀x:int. x + 1 + 2 > 0")));
139151
}
140152

141153
@Test
142154
void recordsOriginWhenOnlyGroupIsUnwrapped() {
143155
VCImplication implication = vc("(x > 0)");
144-
VCImplication result = assertSimplificationSteps(VCFolding::apply, implication, "x > 0");
156+
VCImplication result = assertSimplificationSteps(VCFolding::apply, implication,
157+
chain(expect("x > 0", "x > 0")));
145158

146159
SimplifiedVCImplication simplified = assertInstanceOf(SimplifiedVCImplication.class, result);
147160
assertEquals("x > 0", simplified.getRefinement().toString());
@@ -152,12 +165,14 @@ void recordsOriginWhenOnlyGroupIsUnwrapped() {
152165
void recordsOriginWhenFoldingLaterImplication() {
153166
VCImplication implication = vc("x > 0", "1 + 2 > 0");
154167

155-
VCImplication result = assertSimplificationSteps(VCFolding::apply, implication, "x > 0 -> 3 > 0");
168+
VCImplication result = assertSimplificationSteps(VCFolding::apply, implication,
169+
chain(expect("x > 0", "x > 0"), expect("3 > 0", "1 + 2 > 0")));
156170

157171
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
158172
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());
159173

160-
result = assertSimplificationSteps(VCFolding::apply, result, "x > 0 -> true");
174+
result = assertSimplificationSteps(VCFolding::apply, result,
175+
chain(expect("x > 0", "x > 0"), expect("true", "1 + 2 > 0")));
161176

162177
simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
163178
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());

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

Lines changed: 30 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package liquidjava.rj_language.opt;
22

3-
import static liquidjava.utils.VCTestUtils.assertSimplificationSteps;
4-
import static liquidjava.utils.VCTestUtils.vc;
3+
import static liquidjava.utils.VCTestUtils.*;
54
import static org.junit.jupiter.api.Assertions.assertNull;
65

76
import liquidjava.processor.VCImplication;
@@ -23,67 +22,83 @@ void simplifyOnceReturnsNullForNullImplication() {
2322
void simplifyOnceAppliesSubstitutionBeforeFolding() {
2423
VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2");
2524

26-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "1 + 2 > 2", "3 > 2", "true");
25+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
26+
chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "∀x:int. x > 2")),
27+
chain(expect("true", "∀x:int. x > 2")));
2728
}
2829

2930
@Test
3031
void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() {
3132
VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3");
3233

33-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "1 + 2 == 3", "3 == 3", "true");
34+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
35+
chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "∀x:int. x == 3")),
36+
chain(expect("true", "∀x:int. x == 3")));
3437
}
3538

3639
@Test
3740
void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() {
3841
VCImplication implication = vc("1 + 2 > 2");
3942

40-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "3 > 2", "true");
43+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")),
44+
chain(expect("true", "1 + 2 > 2")));
4145
}
4246

4347
@Test
4448
void simplifyKeepsApplyingStepsUntilFixedPoint() {
4549
VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3");
4650

47-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "1 + 2 + 1 > 3", "3 + 1 > 3", "4 > 3",
48-
"true");
51+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
52+
chain(expect("1 + 2 + 1 > 3", "∀x:int. x + 1 > 3")), chain(expect("3 + 1 > 3", "∀x:int. x + 1 > 3")),
53+
chain(expect("4 > 3", "∀x:int. x + 1 > 3")), chain(expect("true", "∀x:int. x + 1 > 3")));
4954
}
5055

5156
@Test
5257
void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() {
5358
VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");
5459

55-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "∀y:int. y == 3 + 1 -> y > 3",
56-
"3 + 1 > 3", "4 > 3", "true");
60+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
61+
chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")),
62+
chain(expect("3 + 1 > 3", "∀y:int. y > x")), chain(expect("4 > 3", "∀y:int. y > x")),
63+
chain(expect("true", "∀y:int. y > x")));
5764
}
5865

5966
@Test
6067
void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() {
6168
VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3");
6269

6370
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
64-
"∀y:int. y == 1 + 1 -> ∀z:int. z == y + 1 -> z == 3", "∀z:int. z == 1 + 1 + 1 -> z == 3",
65-
"1 + 1 + 1 == 3", "2 + 1 == 3", "3 == 3", "true");
71+
chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1", "∀z:int. z == y + 1"),
72+
expect("z == 3", "z == 3")),
73+
chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3", "z == 3")),
74+
chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "∀z:int. z == 3")),
75+
chain(expect("3 == 3", "∀z:int. z == 3")), chain(expect("true", "∀z:int. z == 3")));
6676
}
6777

6878
@Test
6979
void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
7080
VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2");
7181

72-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "∀y:int. y == 1 + 2 -> y - 1 == 2",
73-
"1 + 2 - 1 == 2", "3 - 1 == 2", "2 == 2", "true");
82+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
83+
chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2", "y - 1 == 2")),
84+
chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")),
85+
chain(expect("3 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("2 == 2", "∀y:int. y - 1 == 2")),
86+
chain(expect("true", "∀y:int. y - 1 == 2")));
7487
}
7588

7689
@Test
7790
void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() {
7891
VCImplication implication = vc("∀x:int. x == a + 0", "x >= -3");
7992

80-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "a + 0 >= -3");
93+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
94+
chain(expect("a + 0 >= -3", "∀x:int. x >= -3")));
8195
}
8296

8397
@Test
8498
void simplifyLeavesUnchangedVcAsPlainPredicates() {
8599
VCImplication implication = vc("x > 0", "y > x");
86100

87-
assertSimplificationSteps(VCSimplification::simplifyOnce, implication, "x > 0 -> y > x");
101+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
102+
chain(expect("x > 0", "x > 0"), expect("y > x", "y > x")));
88103
}
89104
}

0 commit comments

Comments
 (0)