fix: format source.

sosy-lab · Oct 8, 2022 · 6cd9ecc · 6cd9ecc
1 parent 6f6e55b
commit 6cd9ecc
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 13 deletions.
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
@@ -88,7 +88,9 @@ public Term makeVariable(Sort sort, String name) {
     Preconditions.checkArgument(
         sort.equals(exp.getSort()),
         "symbol name %s with sort %s already in use for different sort %s",
-        name, sort, exp.getSort());
+        name,
+        sort,
+        exp.getSort());
     return exp;
   }
 
@@ -228,8 +230,7 @@ public <T extends Formula> T encapsulate(FormulaType<T> pType, Term pTerm) {
             || (pType.equals(FormulaType.RationalType)
                 && getFormulaType(pTerm).equals(FormulaType.IntegerType))
         : String.format(
-            "Cannot encapsulate formula %s of Type %s as %s",
-            pTerm, getFormulaType(pTerm), pType);
+            "Cannot encapsulate formula %s of Type %s as %s", pTerm, getFormulaType(pTerm), pType);
     if (pType.isBooleanType()) {
       return (T) new CVC5BooleanFormula(pTerm);
     } else if (pType.isIntegerType()) {

diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
@@ -163,8 +163,7 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
     } else {
       // Z3 and other solvers support Unicode characters in the theory of strings.
       assertThatFormula(
-              smgr.in(
-                  smgr.makeVariable("x"), smgr.union(smgr.range('a', 'Δ'), regexAllChar)))
+              smgr.in(smgr.makeVariable("x"), smgr.union(smgr.range('a', 'Δ'), regexAllChar)))
           .isSatisfiable();
       // Combining characters are not matched as one character.
       // Non-ascii non-printable characters should use the codepoint representation
@@ -191,30 +190,31 @@ public void testEmptyRegex() throws SolverException, InterruptedException {
   }
 
   @Test
-  public void testRegexUnion() throws  SolverException, InterruptedException {
+  public void testRegexUnion() throws SolverException, InterruptedException {
     RegexFormula regex = smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b"));
     assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isSatisfiable();
     assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isSatisfiable();
     assertThatFormula(smgr.in(smgr.makeString("c"), regex)).isUnsatisfiable();
   }
 
   @Test
-  public void testRegexIntersection() throws  SolverException, InterruptedException {
+  public void testRegexIntersection() throws SolverException, InterruptedException {
     RegexFormula regex = smgr.intersection(smgr.makeRegex("a"), smgr.makeRegex("b"));
     StringFormula variable = smgr.makeVariable("var");
     assertThatFormula(smgr.in(variable, regex)).isUnsatisfiable();
 
-    regex = smgr.intersection(
-        smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")),
-        smgr.union(smgr.makeRegex("b"), smgr.makeRegex("c")));
+    regex =
+        smgr.intersection(
+            smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")),
+            smgr.union(smgr.makeRegex("b"), smgr.makeRegex("c")));
     assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isUnsatisfiable();
     assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isSatisfiable();
   }
 
   @Test
-  public void testRegexDifference() throws  SolverException, InterruptedException {
-    RegexFormula regex = smgr.difference(
-        smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), smgr.makeRegex("b"));
+  public void testRegexDifference() throws SolverException, InterruptedException {
+    RegexFormula regex =
+        smgr.difference(smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), smgr.makeRegex("b"));
     assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isSatisfiable();
     assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isUnsatisfiable();
   }