Skip to content

Commit 96f9842

Browse files
rcosta358rcosta358
committed
Refactor Tests
1 parent 08ec730 commit 96f9842

7 files changed

Lines changed: 106 additions & 249 deletions

File tree

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

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

33
import static liquidjava.utils.VCTestUtils.*;
4-
import liquidjava.processor.VCImplication;
54
import org.junit.jupiter.api.Test;
65

76
class VCArithmeticSimplificationTest {
@@ -57,8 +56,6 @@ void simplifiesOnlyFirstArithmeticIdentity() {
5756

5857
@Test
5958
void recordsOriginWhenSimplifyingLaterImplication() {
60-
VCImplication implication = vc("x > 0", "y + 0 > x");
61-
62-
assertSimplificationSteps(simplification, implication, step("x > 0", "y > x"));
59+
assertSimplificationSteps(simplification, vc("x > 0", "y + 0 > x"), step("x > 0", "y > x"));
6360
}
6461
}

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

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

33
import static liquidjava.utils.VCTestUtils.*;
4-
import static org.junit.jupiter.api.Assertions.assertFalse;
5-
6-
import liquidjava.processor.VCImplication;
74
import org.junit.jupiter.api.Test;
85

96
class VCBinderSimplificationTest {
@@ -12,54 +9,38 @@ class VCBinderSimplificationTest {
129

1310
@Test
1411
void removesTrueBinderWhenVariableIsUnusedDownstream() {
15-
VCImplication implication = vc("∀x:int. true", "y > 0");
16-
17-
assertSimplificationSteps(binderSimplification, implication, step("y > 0"));
12+
assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0"));
1813
}
1914

2015
@Test
2116
void keepsTrueBinderWhenVariableIsUsedDownstream() {
22-
VCImplication implication = vc("∀x:int. true", "x > 0");
23-
24-
assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0"));
17+
assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("true", "x > 0"));
2518
}
2619

2720
@Test
2821
void collapsesFalseBinderSuffixToPlainTrue() {
29-
VCImplication implication = vc("∀x:int. false", "x > 0", "y > 0");
30-
VCImplication result = binderSimplification.apply(implication);
31-
32-
assertFalse(result.hasBinder());
33-
assertSimplifiedVC(result, "true");
22+
assertSimplificationSteps(binderSimplification, vc("∀x:int. false", "y > 0"), step("true"));
3423
}
3524

3625
@Test
3726
void simplifiesOnlyFirstApplicableBinder() {
38-
VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
39-
40-
assertSimplificationSteps(binderSimplification, implication, step("true", "z > 0"));
27+
assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "∀y:int. true", "z > 0"),
28+
step("true", "z > 0"));
4129
}
4230

4331
@Test
4432
void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() {
45-
VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0");
46-
47-
assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0", "z > 0"));
33+
assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"),
34+
step("true", "x > 0", "z > 0"));
4835
}
4936

5037
@Test
5138
void ignoresNonBinderBooleanLiterals() {
52-
VCImplication implication = vc("true", "false");
53-
54-
assertSimplificationSteps(binderSimplification, implication, step("true", "false"));
39+
assertSimplificationSteps(binderSimplification, vc("true", "false"), step("true", "false"));
5540
}
5641

5742
@Test
5843
void trueBinderWithoutSuffixBecomesPlainTrue() {
59-
VCImplication implication = vc("∀x:int. true");
60-
VCImplication result = binderSimplification.apply(implication);
61-
62-
assertFalse(result.hasBinder());
63-
assertSimplifiedVC(result, "true");
44+
assertSimplificationSteps(binderSimplification, vc("∀x:int. true"), step("true"));
6445
}
6546
}

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

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

33
import static liquidjava.utils.VCTestUtils.*;
4-
import static org.junit.jupiter.api.Assertions.assertEquals;
54
import liquidjava.processor.VCImplication;
65
import liquidjava.rj_language.Predicate;
76
import liquidjava.rj_language.ast.BinaryExpression;
@@ -15,19 +14,14 @@ class VCFoldingTest {
1514

1615
@Test
1716
void foldsIntegerArithmeticAndComparisons() {
18-
VCImplication implication = vc("1 + 2 == 3");
19-
20-
assertSimplificationSteps(folding, implication, step("3 == 3"), step("true"));
17+
assertSimplificationSteps(folding, vc("1 + 2 == 3"), step("3 == 3"), step("true"));
2118
assertSimplificationSteps(folding, vc("4 > 7"), step("false"));
2219
}
2320

2421
@Test
2522
void foldsRealAndMixedNumericExpressions() {
26-
VCImplication realArithmetic = vc("1.5 + 2.0 == 3.5");
27-
VCImplication mixedArithmetic = vc("2 + 0.5 > 2");
28-
29-
assertSimplificationSteps(folding, realArithmetic, step("3.5 == 3.5"), step("true"));
30-
assertSimplificationSteps(folding, mixedArithmetic, step("2.5 > 2"), step("true"));
23+
assertSimplificationSteps(folding, vc("1.5 + 2.0 == 3.5"), step("3.5 == 3.5"), step("true"));
24+
assertSimplificationSteps(folding, vc("2 + 0.5 > 2"), step("2.5 > 2"), step("true"));
3125
}
3226

3327
@Test
@@ -44,19 +38,14 @@ void leavesRealDivisionAndModuloByZeroUnchanged() {
4438

4539
@Test
4640
void foldsIntegerDivisionTowardZeroForNegativeResults() {
47-
VCImplication implication = vc("(2 - 7) / 2 == -2");
48-
49-
assertSimplificationSteps(folding, implication, step("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"),
41+
assertSimplificationSteps(folding, vc("(2 - 7) / 2 == -2"), step("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"),
5042
step("-2 == -2"), step("-2 == -2"), step("true"));
5143
}
5244

5345
@Test
5446
void foldsIntegerModuloWithJavaSignedRemainder() {
55-
VCImplication negativeDividend = vc("-5 % 2 < 0");
56-
VCImplication negativeDivisor = vc("5 % -2 > 0");
57-
58-
assertSimplificationSteps(folding, negativeDividend, step("-5 % 2 < 0"), step("-1 < 0"), step("true"));
59-
assertSimplificationSteps(folding, negativeDivisor, step("5 % -2 > 0"), step("1 > 0"), step("true"));
47+
assertSimplificationSteps(folding, vc("-5 % 2 < 0"), step("-5 % 2 < 0"), step("-1 < 0"), step("true"));
48+
assertSimplificationSteps(folding, vc("5 % -2 > 0"), step("5 % -2 > 0"), step("1 > 0"), step("true"));
6049
}
6150

6251
@Test
@@ -85,9 +74,7 @@ void foldsPartialComparisonsWithoutDroppingSymbolicTerms() {
8574
@Test
8675
void foldsUnaryExpressions() {
8776
assertSimplificationSteps(folding, vc("!true"), step("false"));
88-
VCImplication implication = vc("-3 < 0");
89-
90-
assertSimplificationSteps(folding, implication, step("-3 < 0"), step("true"));
77+
assertSimplificationSteps(folding, vc("-3 < 0"), step("-3 < 0"), step("true"));
9178
}
9279

9380
@Test
@@ -99,9 +86,7 @@ void foldsIteExpressions() {
9986

10087
@Test
10188
void foldsIteBranchesBeforeComparingThem() {
102-
VCImplication implication = vc("cond ? 1 + 2 : 3");
103-
104-
assertSimplificationSteps(folding, implication, step("cond ? 3 : 3"), step("3"));
89+
assertSimplificationSteps(folding, vc("cond ? 1 + 2 : 3"), step("cond ? 3 : 3"), step("3"));
10590
}
10691

10792
@Test
@@ -118,6 +103,16 @@ void foldsEnumEqualityAndInequality() {
118103
assertSimplificationSteps(folding, vc("Mode.Photo != Mode.Video"), step("true"));
119104
}
120105

106+
@Test
107+
void recordsOriginWhenOnlyGroupIsUnwrapped() {
108+
assertSimplificationSteps(folding, vc("(x > 0)"), step("x > 0"));
109+
}
110+
111+
@Test
112+
void recordsOriginWhenFoldingLaterImplication() {
113+
assertSimplificationSteps(folding, vc("x > 0", "1 + 2 > 0"), step("x > 0", "3 > 0"), step("x > 0", "true"));
114+
}
115+
121116
@Test
122117
void foldsResolvedEnumLiterals() {
123118
Enum limit = new Enum("Config", "LIMIT");
@@ -138,23 +133,4 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() {
138133

139134
assertSimplificationSteps(folding, implication, step("3 + 2 == 5"), step("5 == 5"), step("true"));
140135
}
141-
142-
@Test
143-
void recordsOriginWhenOnlyGroupIsUnwrapped() {
144-
VCImplication implication = vc("(x > 0)");
145-
VCSimplificationResult result = assertSimplificationSteps(folding, implication, step("x > 0"));
146-
147-
assertEquals("x > 0", result.getImplication().getRefinement().toString());
148-
}
149-
150-
@Test
151-
void recordsOriginWhenFoldingLaterImplication() {
152-
VCImplication implication = vc("x > 0", "1 + 2 > 0");
153-
154-
VCSimplificationResult result = assertSimplificationSteps(folding, implication, step("x > 0", "3 > 0"));
155-
156-
result = assertSimplificationSteps(folding, result.getImplication(), step("x > 0", "true"));
157-
assertEquals("true", result.getImplication().getNext().getRefinement().getExpression().toDisplayString());
158-
}
159-
160136
}

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

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

33
import static liquidjava.utils.VCTestUtils.*;
4-
import liquidjava.processor.VCImplication;
54
import org.junit.jupiter.api.Test;
65

76
class VCLogicalSimplificationTest {
@@ -66,8 +65,6 @@ void simplifiesIteChildren() {
6665

6766
@Test
6867
void recordsOriginWhenSimplifyingLaterImplication() {
69-
VCImplication implication = vc("x > 0", "y || false");
70-
71-
assertSimplificationSteps(simplification, implication, step("x > 0", "y"));
68+
assertSimplificationSteps(simplification, vc("x > 0", "y || false"), step("x > 0", "y"));
7269
}
7370
}

0 commit comments

Comments
 (0)