Skip to content

Commit f841c4c

Browse files
kfriedbergerkfriedberger
committed
simplify test with common variables.
1 parent 08820e3 commit f841c4c

File tree

1 file changed

+39
-62
lines changed

1 file changed

+39
-62
lines changed

‎src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java‎

Lines changed: 39 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -64,12 +64,20 @@ public class StringFormulaManagerTest extends SolverBasedTest0.ParameterizedSolv
6464
"abchurrdurr",
6565
"abcdefaaaaa");
6666

67+
private StringFormula a;
68+
private StringFormula b;
69+
private StringFormula ab;
70+
private StringFormula empty;
6771
private StringFormula hello;
6872
private RegexFormula a2z;
6973

7074
@Before
7175
public void setup() {
7276
requireStrings();
77+
a = smgr.makeString("a");
78+
b = smgr.makeString("b");
79+
ab = smgr.makeString("ab");
80+
empty = smgr.makeString("");
7381
hello = smgr.makeString("hello");
7482
a2z = smgr.range('a', 'z');
7583
}
@@ -129,16 +137,16 @@ public void testRegexAllChar() throws SolverException, InterruptedException {
129137

130138
RegexFormula regexAllChar = smgr.allChar();
131139

132-
assertThatFormula(smgr.in(smgr.makeString("a"), regexAllChar)).isSatisfiable();
133-
assertThatFormula(smgr.in(smgr.makeString("ab"), regexAllChar)).isUnsatisfiable();
134-
assertThatFormula(smgr.in(smgr.makeString(""), regexAllChar)).isUnsatisfiable();
135-
assertThatFormula(smgr.in(smgr.makeString("ab"), smgr.times(regexAllChar, 2))).isSatisfiable();
140+
assertThatFormula(smgr.in(a, regexAllChar)).isSatisfiable();
141+
assertThatFormula(smgr.in(ab, regexAllChar)).isUnsatisfiable();
142+
assertThatFormula(smgr.in(empty, regexAllChar)).isUnsatisfiable();
143+
assertThatFormula(smgr.in(ab, smgr.times(regexAllChar, 2))).isSatisfiable();
136144
assertThatFormula(
137145
smgr.in(smgr.makeVariable("x"), smgr.intersection(smgr.range('9', 'a'), regexAllChar)))
138146
.isSatisfiable();
139147

140148
RegexFormula regexDot = smgr.makeRegex(".");
141-
assertThatFormula(smgr.in(smgr.makeString("a"), regexDot)).isUnsatisfiable();
149+
assertThatFormula(smgr.in(a, regexDot)).isUnsatisfiable();
142150
}
143151

144152
@Test
@@ -169,7 +177,7 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
169177
smgr.in(smgr.makeVariable("x"), smgr.union(smgr.range('a', 'Δ'), regexAllChar)))
170178
.isSatisfiable();
171179
// Combining characters are not matched as one character.
172-
// Non-ascii non-printable characters should use the codepoint representation
180+
// Non-ascii non-printable characters should use the codePoint representation
173181
assertThatFormula(smgr.in(smgr.makeString("Δ"), regexAllChar)).isUnsatisfiable();
174182
}
175183
}
@@ -197,8 +205,8 @@ public void testEmptyRegex() throws SolverException, InterruptedException {
197205
@Test
198206
public void testRegexUnion() throws SolverException, InterruptedException {
199207
RegexFormula regex = smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b"));
200-
assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isSatisfiable();
201-
assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isSatisfiable();
208+
assertThatFormula(smgr.in(a, regex)).isSatisfiable();
209+
assertThatFormula(smgr.in(b, regex)).isSatisfiable();
202210
assertThatFormula(smgr.in(smgr.makeString("c"), regex)).isUnsatisfiable();
203211
}
204212

@@ -212,16 +220,16 @@ public void testRegexIntersection() throws SolverException, InterruptedException
212220
smgr.intersection(
213221
smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")),
214222
smgr.union(smgr.makeRegex("b"), smgr.makeRegex("c")));
215-
assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isUnsatisfiable();
216-
assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isSatisfiable();
223+
assertThatFormula(smgr.in(a, regex)).isUnsatisfiable();
224+
assertThatFormula(smgr.in(b, regex)).isSatisfiable();
217225
}
218226

219227
@Test
220228
public void testRegexDifference() throws SolverException, InterruptedException {
221229
RegexFormula regex =
222230
smgr.difference(smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), smgr.makeRegex("b"));
223-
assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isSatisfiable();
224-
assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isUnsatisfiable();
231+
assertThatFormula(smgr.in(a, regex)).isSatisfiable();
232+
assertThatFormula(smgr.in(b, regex)).isUnsatisfiable();
225233
}
226234

227235
@Test
@@ -236,8 +244,6 @@ public void testStringConcat() throws SolverException, InterruptedException {
236244

237245
@Test
238246
public void testStringConcatEmpty() throws SolverException, InterruptedException {
239-
StringFormula empty = smgr.makeString("");
240-
241247
assertEqual(empty, smgr.concat(ImmutableList.of()));
242248
assertEqual(empty, smgr.concat(empty));
243249
assertEqual(empty, smgr.concat(empty, empty));
@@ -317,13 +323,13 @@ public void testStringToIntConversionCornerCases() throws SolverException, Inter
317323
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("-123")));
318324
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("-1234")));
319325

320-
assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("")));
321-
assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("a")));
326+
assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(empty));
327+
assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(a));
322328
assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("1a")));
323329
assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("a1")));
324330

325-
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("")));
326-
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("a")));
331+
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(empty));
332+
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(a));
327333
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("1a")));
328334
assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("a1")));
329335
}
@@ -333,21 +339,21 @@ public void testIntToStringConversionCornerCases() throws SolverException, Inter
333339
assertEqual(smgr.makeString("123"), smgr.toStringFormula(imgr.makeNumber(123)));
334340
assertEqual(smgr.makeString("1"), smgr.toStringFormula(imgr.makeNumber(1)));
335341
assertEqual(smgr.makeString("0"), smgr.toStringFormula(imgr.makeNumber(0)));
336-
assertEqual(smgr.makeString(""), smgr.toStringFormula(imgr.makeNumber(-1)));
337-
assertEqual(smgr.makeString(""), smgr.toStringFormula(imgr.makeNumber(-123)));
342+
assertEqual(empty, smgr.toStringFormula(imgr.makeNumber(-1)));
343+
assertEqual(empty, smgr.toStringFormula(imgr.makeNumber(-123)));
338344

339345
assertDistinct(smgr.makeString("1"), smgr.toStringFormula(imgr.makeNumber(-1)));
340346
}
341347

342348
@Test
343349
public void testStringLength() throws SolverException, InterruptedException {
344-
assertEqual(imgr.makeNumber(0), smgr.length(smgr.makeString("")));
345-
assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("a")));
350+
assertEqual(imgr.makeNumber(0), smgr.length(empty));
351+
assertEqual(imgr.makeNumber(1), smgr.length(a));
346352
assertEqual(imgr.makeNumber(2), smgr.length(smgr.makeString("aa")));
347353
assertEqual(imgr.makeNumber(9), smgr.length(smgr.makeString("aaabbbccc")));
348354

349-
assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("")));
350-
assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("a")));
355+
assertDistinct(imgr.makeNumber(5), smgr.length(empty));
356+
assertDistinct(imgr.makeNumber(5), smgr.length(a));
351357
assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("aa")));
352358
assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("aaabbbcc")));
353359
}
@@ -357,7 +363,7 @@ public void testStringLengthWithVariable() throws SolverException, InterruptedEx
357363
StringFormula var = smgr.makeVariable("var");
358364

359365
assertThatFormula(imgr.equal(imgr.makeNumber(0), smgr.length(var)))
360-
.implies(smgr.equal(var, smgr.makeString("")));
366+
.implies(smgr.equal(var, empty));
361367

362368
assertThatFormula(
363369
bmgr.and(
@@ -376,15 +382,15 @@ public void testStringLengthWithVariable() throws SolverException, InterruptedEx
376382
assertThatFormula(
377383
bmgr.and(
378384
imgr.equal(imgr.makeNumber(4), smgr.length(var)),
379-
smgr.prefix(smgr.makeString("ab"), var),
385+
smgr.prefix(ab, var),
380386
smgr.suffix(smgr.makeString("ba"), var),
381387
smgr.equal(smgr.makeString("c"), smgr.charAt(var, imgr.makeNumber(3)))))
382388
.isUnsatisfiable();
383389

384390
assertThatFormula(
385391
bmgr.and(
386392
imgr.equal(imgr.makeNumber(5), smgr.length(var)),
387-
smgr.prefix(smgr.makeString("ab"), var),
393+
smgr.prefix(ab, var),
388394
smgr.suffix(smgr.makeString("ba"), var),
389395
smgr.equal(smgr.makeString("c"), smgr.charAt(var, imgr.makeNumber(3)))))
390396
.implies(smgr.equal(smgr.makeVariable("var"), smgr.makeString("abcba")));
@@ -567,14 +573,14 @@ public void testStringLengthInequalityNegativeRange()
567573
bmgr.and(
568574
imgr.lessOrEquals(minusTenThousand, stringVariableLength),
569575
imgr.lessOrEquals(stringVariableLength, zero),
570-
bmgr.not(smgr.equal(stringVariable, smgr.makeString("")))))
576+
bmgr.not(smgr.equal(stringVariable, empty))))
571577
.isUnsatisfiable();
572578
// -10000 <= stringVariable length <= 0 -> SAT implies stringVariable = ""
573579
assertThatFormula(
574580
bmgr.and(
575581
imgr.lessOrEquals(minusTenThousand, stringVariableLength),
576582
imgr.lessOrEquals(stringVariableLength, zero)))
577-
.implies(smgr.equal(stringVariable, smgr.makeString("")));
583+
.implies(smgr.equal(stringVariable, empty));
578584
}
579585

580586
/**
@@ -615,7 +621,7 @@ public void testStringLengthInequalityPositiveRange()
615621
bmgr.and(
616622
imgr.lessOrEquals(zero, stringVariableLength),
617623
imgr.lessThan(stringVariableLength, one)))
618-
.implies(smgr.equal(stringVariable, smgr.makeString("")));
624+
.implies(smgr.equal(stringVariable, empty));
619625
// 1 < stringVariable length < 3 -> SAT implies stringVariable length = 2
620626
assertThatFormula(
621627
bmgr.and(
@@ -649,9 +655,6 @@ public void testSimpleConstStringLexicographicOrdering()
649655
@Test
650656
public void testSimpleStringVariableLexicographicOrdering()
651657
throws SolverException, InterruptedException {
652-
StringFormula a = smgr.makeString("a");
653-
StringFormula b = smgr.makeString("b");
654-
StringFormula ab = smgr.makeString("ab");
655658
StringFormula abc = smgr.makeString("abc");
656659
StringFormula abd = smgr.makeString("abd");
657660
StringFormula abe = smgr.makeString("abe");
@@ -665,14 +668,14 @@ public void testSimpleStringVariableLexicographicOrdering()
665668
smgr.lessThan(a, stringVariable),
666669
smgr.lessThan(stringVariable, b),
667670
imgr.equal(imgr.makeNumber(0), smgr.length(stringVariable))))
668-
.implies(smgr.equal(stringVariable, smgr.makeString("")));
671+
.implies(smgr.equal(stringVariable, empty));
669672

670673
assertThatFormula(
671674
bmgr.and(
672675
smgr.lessOrEquals(a, stringVariable),
673676
smgr.lessThan(stringVariable, b),
674677
imgr.equal(imgr.makeNumber(1), smgr.length(stringVariable))))
675-
.implies(smgr.equal(stringVariable, smgr.makeString("a")));
678+
.implies(smgr.equal(stringVariable, a));
676679

677680
assertThatFormula(
678681
bmgr.and(
@@ -715,11 +718,6 @@ public void testSimpleStringVariableLexicographicOrdering()
715718
/** Takeaway: invalid positions always refer to the empty string! */
716719
@Test
717720
public void testCharAtWithConstString() throws SolverException, InterruptedException {
718-
StringFormula empty = smgr.makeString("");
719-
StringFormula a = smgr.makeString("a");
720-
StringFormula b = smgr.makeString("b");
721-
StringFormula ab = smgr.makeString("ab");
722-
723721
assertEqual(smgr.charAt(empty, imgr.makeNumber(1)), empty);
724722
assertEqual(smgr.charAt(empty, imgr.makeNumber(0)), empty);
725723
assertEqual(smgr.charAt(empty, imgr.makeNumber(-1)), empty);
@@ -762,8 +760,6 @@ public void testCharAtWithSpecialCharacters() throws SolverException, Interrupte
762760
String workaround = "au{1234}";
763761
StringFormula au1234WOEscapeCurly = smgr.makeString(workaround);
764762
StringFormula backSlash = smgr.makeString("\\");
765-
StringFormula a = smgr.makeString("a");
766-
StringFormula b = smgr.makeString("b");
767763
StringFormula u1234 = smgr.makeString("\\u{1234}");
768764
StringFormula au1234b = smgr.makeString("a\\u{1234}b");
769765
StringFormula stringVariable = smgr.makeVariable("stringVariable");
@@ -827,8 +823,6 @@ public void testCharAtWithSpecialCharacters2Byte() throws SolverException, Inter
827823
String workaround = "au{7B}";
828824
StringFormula acurlyOpen2BUnicodeWOEscapeCurly = smgr.makeString(workaround);
829825
// StringFormula backSlash = smgr.makeString("\\");
830-
StringFormula a = smgr.makeString("a");
831-
StringFormula b = smgr.makeString("b");
832826
StringFormula stringVariable = smgr.makeVariable("stringVariable");
833827

834828
// Curly braces unicode is treated as 1 char
@@ -870,9 +864,6 @@ public void testCharAtWithSpecialCharacters2Byte() throws SolverException, Inter
870864

871865
@Test
872866
public void testCharAtWithStringVariable() throws SolverException, InterruptedException {
873-
StringFormula a = smgr.makeString("a");
874-
StringFormula b = smgr.makeString("b");
875-
StringFormula ab = smgr.makeString("ab");
876867
StringFormula aa = smgr.makeString("aa");
877868
StringFormula abc = smgr.makeString("abc");
878869
StringFormula aabc = smgr.makeString("aabc");
@@ -931,11 +922,8 @@ public void testCharAtWithStringVariable() throws SolverException, InterruptedEx
931922

932923
@Test
933924
public void testConstStringContains() throws SolverException, InterruptedException {
934-
StringFormula empty = smgr.makeString("");
935-
StringFormula a = smgr.makeString("a");
936925
StringFormula aUppercase = smgr.makeString("A");
937926
StringFormula bUppercase = smgr.makeString("B");
938-
StringFormula b = smgr.makeString("b");
939927
StringFormula bbbbbb = smgr.makeString("bbbbbb");
940928
StringFormula bbbbbbb = smgr.makeString("bbbbbbb");
941929
StringFormula abbbbbb = smgr.makeString("abbbbbb");
@@ -981,9 +969,7 @@ public void testStringVariableContains() throws SolverException, InterruptedExce
981969
StringFormula var1 = smgr.makeVariable("var1");
982970
StringFormula var2 = smgr.makeVariable("var2");
983971

984-
StringFormula empty = smgr.makeString("");
985972
StringFormula bUppercase = smgr.makeString("B");
986-
StringFormula ab = smgr.makeString("ab");
987973
StringFormula bbbbbb = smgr.makeString("bbbbbb");
988974
StringFormula abbbbbb = smgr.makeString("abbbbbb");
989975
StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
@@ -1032,7 +1018,6 @@ public void testStringContainsOtherVariable() throws SolverException, Interrupte
10321018
StringFormula var2 = smgr.makeVariable("var2");
10331019

10341020
StringFormula abUppercase = smgr.makeString("AB");
1035-
StringFormula ab = smgr.makeString("ab");
10361021

10371022
assertThatFormula(
10381023
bmgr.and(
@@ -1044,11 +1029,7 @@ public void testStringContainsOtherVariable() throws SolverException, Interrupte
10441029

10451030
@Test
10461031
public void testConstStringIndexOf() throws SolverException, InterruptedException {
1047-
StringFormula empty = smgr.makeString("");
1048-
StringFormula a = smgr.makeString("a");
10491032
StringFormula aUppercase = smgr.makeString("A");
1050-
StringFormula b = smgr.makeString("b");
1051-
StringFormula ab = smgr.makeString("ab");
10521033
StringFormula bbbbbb = smgr.makeString("bbbbbb");
10531034
StringFormula bbbbbbb = smgr.makeString("bbbbbbb");
10541035
StringFormula abbbbbb = smgr.makeString("abbbbbb");
@@ -1097,7 +1078,6 @@ public void testStringVariableIndexOf() throws SolverException, InterruptedExcep
10971078
StringFormula var2 = smgr.makeVariable("var2");
10981079
IntegerFormula intVar = imgr.makeVariable("intVar");
10991080

1100-
StringFormula empty = smgr.makeString("");
11011081
StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
11021082

11031083
IntegerFormula zero = imgr.makeNumber(0);
@@ -1166,7 +1146,7 @@ public void testStringIndexOfWithSubStrings() throws SolverException, Interrupte
11661146
bmgr.and(
11671147
smgr.contains(var1, smgr.makeString("abba")),
11681148
imgr.equal(imgr.makeNumber(1), smgr.indexOf(var1, smgr.makeString("bba"), zero)),
1169-
imgr.equal(imgr.makeNumber(1), smgr.indexOf(var1, smgr.makeString("b"), zero)),
1149+
imgr.equal(imgr.makeNumber(1), smgr.indexOf(var1, b, zero)),
11701150
imgr.equal(imgr.makeNumber(2), smgr.indexOf(var1, smgr.makeString("ba"), zero))));
11711151
}
11721152

@@ -1198,8 +1178,6 @@ public void testStringPrefixImpliesPrefixIndexOf() throws SolverException, Inter
11981178

11991179
@Test
12001180
public void testConstStringSubStrings() throws SolverException, InterruptedException {
1201-
StringFormula empty = smgr.makeString("");
1202-
StringFormula a = smgr.makeString("a");
12031181
StringFormula aUppercase = smgr.makeString("A");
12041182
StringFormula bUppercase = smgr.makeString("B");
12051183
StringFormula bbbbbb = smgr.makeString("bbbbbb");
@@ -1248,7 +1226,6 @@ public void testConstStringAllPossibleSubStrings() throws SolverException, Inter
12481226
@Test
12491227
public void testStringSubstringOutOfBounds() throws SolverException, InterruptedException {
12501228
StringFormula bbbbbb = smgr.makeString("bbbbbb");
1251-
StringFormula b = smgr.makeString("b");
12521229
StringFormula abbbbbb = smgr.makeString("abbbbbb");
12531230

12541231
StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");

0 commit comments

Comments
 (0)