Clean up code (Improve comments, format, add private default constructor for class only used statically and remove not thrown exceptions)

Author: BaierD

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -25,10 +25,23 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.Appender;
 import org.sosy_lab.common.Appenders;
-import org.sosy_lab.java_smt.api.*;
+import org.sosy_lab.java_smt.api.ArrayFormulaManager;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.EnumerationFormulaManager;
+import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.api.FunctionDeclaration;
+import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
+import org.sosy_lab.java_smt.api.IntegerFormulaManager;
+import org.sosy_lab.java_smt.api.RationalFormulaManager;
+import org.sosy_lab.java_smt.api.SLFormulaManager;
+import org.sosy_lab.java_smt.api.StringFormulaManager;
+import org.sosy_lab.java_smt.api.Tactic;
 import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.TraversalProcess;

src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java

@@ -14,8 +14,11 @@
 import java.util.List;
 import java.util.Optional;
 
-/** Helper class for splitting up an SMT-LIB2 file into a string of commands */
+/** Helper class for splitting up an SMT-LIB2 file into a string of commands. */
 public class Tokenizer {
+
+  private Tokenizer() {}
+
   /**
    * Split up a sequence of lisp expressions.
    *

src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java

@@ -71,7 +71,7 @@ public Integer parseImpl(String pS) throws IllegalArgumentException {
     return yices_parse_term(pS);
   }
 
-  /** Helper function to (pretty) print yices2 sorts */
+  /** Helper function to (pretty) print yices2 sorts. */
   private String getTypeRepr(int type) {
     if (yices_type_is_bitvector(type)) {
       return "(_ BitVec " + yices_bvtype_size(type) + ")";

src/org/sosy_lab/java_smt/test/SanitizerTest.java

@@ -77,7 +77,7 @@ public void exitAtTheEnd() throws SolverException, InterruptedException {
   }
 
   @Test
-  public void stackPushTest() throws SolverException, InterruptedException {
+  public void stackPushTest() {
     // FIXME: We currently don't support stack operations and expect an exceptions to be thrown for
     // these inputs
 

src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java

@@ -481,9 +481,7 @@ private void checkThatAssertIsInLastLine(String dump) {
     TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
 
     String lastCommand = getLast(Tokenizer.tokenize(dump));
-    assertWithMessage("last line(s) of <\n" + dump + ">")
-        .that(lastCommand)
-        .startsWith("(assert ");
+    assertWithMessage("last line(s) of <\n" + dump + ">").that(lastCommand).startsWith("(assert ");
     assertWithMessage("last line(s) of <\n" + dump + ">").that(lastCommand).endsWith(")");
   }