Skip to content

Commit ce8e2b7

Browse files
DavidGalllobDavidGalllob
committed
reformated
1 parent 9de0813 commit ce8e2b7

File tree

6 files changed

+42
-37
lines changed

6 files changed

+42
-37
lines changed

‎src/org/sosy_lab/java_smt/basicimpl/StringGenerator.java‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
import java.util.ArrayList;
1010
import java.util.List;
1111
import java.util.function.Function;
12-
import java.util.regex.Pattern;
1312
import org.sosy_lab.java_smt.api.BooleanFormula;
1413
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
1514
import org.sosy_lab.java_smt.api.RegexFormula;
@@ -40,7 +39,6 @@ protected static void logMakeString(Object result, String value) {
4039
Generator.getExecutedAggregator().add(newEntry);
4140
}
4241

43-
4442
protected static void logMakeRegex(Object result, String value) {
4543
Generator.throwExceptionWhenParameterIsNull(ImmutableList.of(result, value));
4644
List<Object> params = ImmutableList.of(value);
@@ -59,7 +57,6 @@ protected static void logMakeRegex(Object result, String value) {
5957
Generator.getExecutedAggregator().add(newEntry);
6058
}
6159

62-
6360
protected static void logMakeVariable(Object result, String pVar) {
6461
Generator.throwExceptionWhenParameterIsNull(ImmutableList.of(result, pVar));
6562
List<Object> inputParams = new ArrayList<>();
@@ -178,8 +175,6 @@ protected static void logReplaceAll(
178175
logOperation(result, inputParams, "(str.replaceall %s %s %s)", Keyword.SKIP);
179176
}
180177

181-
182-
183178
protected static void logRegexAll(RegexFormula result) {
184179
logOperation(result, ImmutableList.of(), "(re.all)", Keyword.SKIP);
185180
}

‎src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1733,7 +1733,8 @@ && isInteger(operators.get(1))) {
17331733
throw new ParserException("str.to_re requires exactly 1 operand.");
17341734
}
17351735
String reInString = getOperandsAsString(ctx, operands).get(0);
1736-
String regexContent = reInString.substring(1, reInString.length() - 1).replace("\"\"", "\"");
1736+
String regexContent =
1737+
reInString.substring(1, reInString.length() - 1).replace("\"\"", "\"");
17371738
return Objects.requireNonNull(smgr).makeRegex(regexContent);
17381739
case "str.is_digit":
17391740
throw new UnsupportedOperationException("str.is_digit is not supported in JavaSMT");

‎src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessStringFormulaManager.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66
package org.sosy_lab.java_smt.solvers.SolverLess;
77

88
import java.util.List;
9-
import java.util.regex.Pattern;
109
import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
1110

1211
public class SolverLessStringFormulaManager

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -386,7 +386,6 @@ public void testComplexFP2()
386386
assertThat(proverEnvironment.isUnsat()).isFalse();
387387
}
388388

389-
390389
@Test
391390
public void testDeclareFloatingPointsWithBitVectors()
392391
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {

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

Lines changed: 34 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -107,18 +107,15 @@ public void testStringConcatenation()
107107
public void testStringConcatenationWithValues()
108108
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
109109
requireStrings();
110-
String x =
111-
"(declare-const d String)\n"
112-
+ "(assert (= d (str.++ \"a\" \"b\" \"c\")))\n";
110+
String x = "(declare-const d String)\n" + "(assert (= d (str.++ \"a\" \"b\" \"c\")))\n";
113111

114112
BooleanFormula actualResult = mgr.universalParseFromString(x);
115113
StringFormula a = smgr.makeString("a");
116114
StringFormula b = smgr.makeString("b");
117115
StringFormula c = smgr.makeString("c");
118116
StringFormula d = smgr.makeVariable("d");
119117

120-
121-
BooleanFormula constraint = smgr.equal(d, smgr.concat(a,b,c));
118+
BooleanFormula constraint = smgr.equal(d, smgr.concat(a, b, c));
122119

123120
assertThat(actualResult).isEqualTo(constraint);
124121
}
@@ -253,8 +250,9 @@ public void testRegexInRe()
253250
RegexFormula regex = smgr.concat(smgr.makeRegex("a"), smgr.makeRegex("b"));
254251
BooleanFormula regexMatch = smgr.in(a, regex);
255252

256-
assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (str.to_re "
257-
+ "\"\\Qb\\E\")))"));
253+
assertThat(
254+
actualResult.equals(
255+
"(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (str.to_re " + "\"\\Qb\\E\")))"));
258256
}
259257

260258
@Test
@@ -299,8 +297,9 @@ public void testRegexConcat()
299297
RegexFormula regex = smgr.concat(smgr.makeRegex("a"), smgr.makeRegex("b"));
300298
BooleanFormula regexMatch = smgr.in(a, regex);
301299

302-
assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (str.to_re "
303-
+ "\"\\Qb\\E\")))"));
300+
assertThat(
301+
actualResult.equals(
302+
"(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (str.to_re " + "\"\\Qb\\E\")))"));
304303
}
305304

306305
@Test
@@ -313,7 +312,9 @@ public void testRegexUnion()
313312

314313
BooleanFormula actualResult = mgr.universalParseFromString(x);
315314

316-
assertThat(actualResult.equals("(str.in_re a (re.union (str.to_re \"\\Qa\\E\") (str.to_re \"\\Qb\\E\")))"));
315+
assertThat(
316+
actualResult.equals(
317+
"(str.in_re a (re.union (str.to_re \"\\Qa\\E\") (str.to_re \"\\Qb\\E\")))"));
317318
}
318319

319320
@Test
@@ -359,8 +360,9 @@ public void testRegexIntersection()
359360
RegexFormula regex = smgr.intersection(smgr.makeRegex("a"), smgr.makeRegex("b"));
360361
BooleanFormula regexMatch = smgr.in(a, regex);
361362

362-
assertThat(actualResult.equals("(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (str.to_re "
363-
+ "\"\\Qb\\E\")))"));
363+
assertThat(
364+
actualResult.equals(
365+
"(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (str.to_re " + "\"\\Qb\\E\")))"));
364366
}
365367

366368
@Test
@@ -387,8 +389,10 @@ public void testRegexDifference()
387389
+ "(assert (str.in_re a (re.diff (str.to_re \"a\") (str.to_re \"b\"))))\n";
388390

389391
BooleanFormula actualResult = mgr.universalParseFromString(x);
390-
assertThat(actualResult.equals("(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (re.comp (str"
391-
+ ".to_re \"\\Qb\\E\"))))"));
392+
assertThat(
393+
actualResult.equals(
394+
"(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (re.comp (str"
395+
+ ".to_re \"\\Qb\\E\"))))"));
392396
}
393397

394398
@Test
@@ -398,7 +402,9 @@ public void testRegexCross()
398402
String x = "(declare-const a String)\n" + "(assert (str.in_re a (re.+ (str.to_re \"a\"))))\n";
399403

400404
BooleanFormula actualResult = mgr.universalParseFromString(x);
401-
assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (re.* (str.to_re \"\\Qa\\E\"))))"));
405+
assertThat(
406+
actualResult.equals(
407+
"(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (re.* (str.to_re \"\\Qa\\E\"))))"));
402408
}
403409

404410
@Test
@@ -408,8 +414,9 @@ public void testRegexOptional()
408414
String x = "(declare-const a String)\n" + "(assert (str.in_re a (re.opt (str.to_re \"a\"))))\n";
409415

410416
BooleanFormula actualResult = mgr.universalParseFromString(x);
411-
assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (re.* (str.to_re "
412-
+ "\"\\Qa\\E\")))))"));
417+
assertThat(
418+
actualResult.equals(
419+
"(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (re.* (str.to_re " + "\"\\Qa\\E\")))))"));
413420
}
414421

415422
@Test
@@ -485,28 +492,30 @@ public void testDeclareUFString()
485492
@Test
486493
public void testComplexStringRegex()
487494
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
488-
String x = "(declare-const X String)\n"
489-
+ "(assert (not (str.in_re X (re.++ (str.to_re \"/filename=\") (re.* (re.comp (str.to_re \"\\u{a}\"))) (str.to_re \".otf/i\\u{a}\")))))\n"
490-
+ "(assert (str.in_re X (re.++ (str.to_re \"/filename=\") (re.* (re.comp (str.to_re \"\\u{a}\"))) (str.to_re \".xlw/i\\u{a}\"))))\n"
491-
+ "(check-sat)";
495+
String x =
496+
"(declare-const X String)\n"
497+
+ "(assert (not (str.in_re X (re.++ (str.to_re \"/filename=\") (re.* (re.comp"
498+
+ " (str.to_re \"\\u{a}\"))) (str.to_re \".otf/i\\u{a}\")))))\n"
499+
+ "(assert (str.in_re X (re.++ (str.to_re \"/filename=\") (re.* (re.comp (str.to_re"
500+
+ " \"\\u{a}\"))) (str.to_re \".xlw/i\\u{a}\"))))\n"
501+
+ "(check-sat)";
492502
parseGenerateReparseAndCheckSat(x, false);
493503
}
494504

495505
private void parseGenerateReparseAndCheckSat(String pX, boolean isUnsat)
496506
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
497507
BooleanFormula parse = mgr.universalParseFromString(pX);
498-
System.out.println(parse+"\n--------\n");
508+
System.out.println(parse + "\n--------\n");
499509
Generator.assembleConstraint(parse);
500510
String reparsed = Generator.getSMTLIB2String();
501511
System.out.println(reparsed);
502512
BooleanFormula result = mgr.universalParseFromString(reparsed);
503513
ProverEnvironment proverEnvironment = context.newProverEnvironment();
504514
proverEnvironment.addConstraint(result);
505-
if(isUnsat) {
515+
if (isUnsat) {
506516
assertThat(proverEnvironment.isUnsat()).isTrue();
507-
}else{
517+
} else {
508518
assertThat(proverEnvironment.isUnsat()).isFalse();
509519
}
510-
511520
}
512521
}

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

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -137,8 +137,10 @@ public void testRegexMultipleConcat() {
137137
RegexFormula c = Objects.requireNonNull(smgr).makeRegex("c");
138138
StringFormula d = Objects.requireNonNull(smgr).makeVariable("d");
139139
BooleanFormula result = smgr.in(d, smgr.concatRegex(List.of(a, b, c)));
140-
String expectedResult = "(declare-const d String)\n"
141-
+ "(assert (str.in_re d (re.++ (str.to_re \"a\") (str.to_re \"b\") (str.to_re \"c\"))))\n";
140+
String expectedResult =
141+
"(declare-const d String)\n"
142+
+ "(assert (str.in_re d (re.++ (str.to_re \"a\") (str.to_re \"b\") (str.to_re"
143+
+ " \"c\"))))\n";
142144
Generator.assembleConstraint(result);
143145
String actualResult = String.valueOf(Generator.getLines());
144146
assertThat(actualResult).isEqualTo(expectedResult);
@@ -213,8 +215,8 @@ public void testInRegex() {
213215

214216
String actualResult = String.valueOf(Generator.getLines());
215217

216-
String expectedResult = "(declare-const str String)\n"
217-
+ "(assert (str.in_re str (str.to_re \".*test.*\")))\n";
218+
String expectedResult =
219+
"(declare-const str String)\n" + "(assert (str.in_re str (str.to_re \".*test.*\")))\n";
218220

219221
assertThat(actualResult).isEqualTo(expectedResult);
220222
}

0 commit comments

Comments
 (0)