Code style: apply several smaller improvements.

Author: kfriedberger

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

@@ -345,24 +345,21 @@ public R visitFunction(
         Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration) {
       switch (functionDeclaration.getKind()) {
         case AND:
-          R out = delegate.visitAnd(getBoolArgs(args));
-          return out;
+          return delegate.visitAnd(getBoolArgs(args));
         case NOT:
           checkState(args.size() == 1);
           Formula arg = args.get(0);
 
           checkArgument(arg instanceof BooleanFormula);
           return delegate.visitNot((BooleanFormula) arg);
         case OR:
-          R out2 = delegate.visitOr(getBoolArgs(args));
-          return out2;
+          return delegate.visitOr(getBoolArgs(args));
         case IFF:
           checkState(args.size() == 2);
           Formula a = args.get(0);
           Formula b = args.get(1);
           checkState(a instanceof BooleanFormula && b instanceof BooleanFormula);
-          R out3 = delegate.visitEquivalence((BooleanFormula) a, (BooleanFormula) b);
-          return out3;
+          return delegate.visitEquivalence((BooleanFormula) a, (BooleanFormula) b);
         case EQ:
           if (args.size() == 2
               && args.get(0) instanceof BooleanFormula

src/org/sosy_lab/java_smt/example/SolverOverviewTable.java

@@ -88,8 +88,7 @@ public static void main(String[] args) throws SolverException, InterruptedExcept
    * UnsatCoreWithAssumptions, Assumptions, AllSat, Interpolation
    *
    * @param context SolverContext you want to check for features.
-   * @return String with the features of the entered solver separated by a comma. Empty if none
-   *     available.
+   * @return supported features of the entered solver separated by a comma. Empty if none available.
    */
   @SuppressWarnings({"CheckReturnValue", "resource"})
   private List<String> getFeatures(SolverContext context)
@@ -158,7 +157,7 @@ private List<String> getFeatures(SolverContext context)
    * as String with each theory separated by a comma.
    *
    * @param context JavaSMT SolverContext of the Solver you want to check for theories.
-   * @return String of all supported theories except Booleans, separated by a comma. Empty if none
+   * @return supported theories except Boolean theory, separated by a comma. Empty if none
    *     available.
    */
   private List<String> getTheories(SolverContext context) {
@@ -323,20 +322,20 @@ private void padLines(List<String> linesToPad, int amountOfLines) {
     private List<String> formatLines(String lineToSplit, int maxLength) {
       List<String> versionSplit = Splitter.on(" ").splitToList(lineToSplit);
       List<String> versionLines = new ArrayList<>();
-      String line = versionSplit.get(0);
+      StringBuilder line = new StringBuilder(versionSplit.get(0));
       int lineCounter = line.length();
       for (String current : Iterables.skip(versionSplit, 1)) {
         lineCounter += current.length() + 1;
 
         if (lineCounter > maxLength) {
           lineCounter = current.length() + 1;
-          versionLines.add(line);
-          line = current;
+          versionLines.add(line.toString());
+          line = new StringBuilder(current);
         } else {
-          line = line + " " + current;
+          line.append(" ").append(current);
         }
       }
-      versionLines.add(line);
+      versionLines.add(line.toString());
       return versionLines;
     }
 

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java

@@ -134,7 +134,7 @@ private Collection<ValueAssignment> getArrayAssignments(Term pTerm, List<Object>
       Vector_Term children = array.children();
       List<Object> innerIndices = new ArrayList<>(upperIndices);
       String name = getArrayName(array);
-      assert name != null;
+      Preconditions.checkNotNull(name, "unexpected array %s without name", array);
       if (children.isEmpty()) {
         // Empty array
         return assignments;

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java

@@ -93,7 +93,7 @@
 public final class BitwuzlaSolverContext extends AbstractSolverContext {
 
   @org.sosy_lab.common.configuration.Options(prefix = "solver.bitwuzla")
-  public static class BitwuzlaSettings {
+  static class BitwuzlaSettings {
 
     enum SatSolver {
       LINGELING,
@@ -117,11 +117,11 @@ enum SatSolver {
                 + "Example: \"PRODUCE_MODELS=2,SAT_SOLVER=kissat\".")
     private String furtherOptions = "";
 
-    protected SatSolver getSatSolver() {
+    SatSolver getSatSolver() {
       return satSolver;
     }
 
-    protected String getFurtherOptions() {
+    String getFurtherOptions() {
       return furtherOptions;
     }
 

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java

@@ -325,8 +325,7 @@ protected Object transformStringToBigInt(String value) {
    */
   private BigInteger parseBigInt(String assignment) {
     try {
-      BigInteger bigInt = new BigInteger(assignment, 2);
-      return bigInt;
+      return new BigInteger(assignment, 2);
     } catch (NumberFormatException e) {
       char[] charArray = assignment.toCharArray();
       for (int i = 0; i < charArray.length; i++) {

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java

@@ -214,7 +214,7 @@ private ImmutableList<ValueAssignment> toList1(Set<String> variables) {
   private ValueAssignment getConstAssignment(long key, String name) {
     List<Object> argumentInterpretation = new ArrayList<>();
     Object value = creator.convertValue(key, evalImpl(key));
-    Long valueNode = BtorJNI.boolector_get_value(btor, key);
+    long valueNode = BtorJNI.boolector_get_value(btor, key);
     // Boolector might return the internal name of the variable with a leading BTOR_number@ which we
     // need to strip!
     return new ValueAssignment(
@@ -232,7 +232,7 @@ private ImmutableList<ValueAssignment> getUFAssignments(long key, String name) {
     // of values may differ when calling boolector_uf_assignment_helper again to get the arguments!
     // The "value" from boolector_get_value() is just
     // a plain copy of the entered node with static results!
-    Long fun = BtorJNI.boolector_get_value(btor, key);
+    long fun = BtorJNI.boolector_get_value(btor, key);
     String[][] ufAssignments = BtorJNI.boolector_uf_assignment_helper(btor, key);
     for (int i = 0; i < ufAssignments[0].length; i++) {
       ImmutableList.Builder<Object> argBuilder = ImmutableList.builder();
@@ -265,7 +265,7 @@ private ValueAssignment getArrayAssignment(long key, String name) {
       argumentInterpretation.add(bfCreator.transformStringToBigInt(stringArrayEntry));
     }
     Object value = creator.convertValue(key, evalImpl(key));
-    Long valueNode = BtorJNI.boolector_get_value(btor, key);
+    long valueNode = BtorJNI.boolector_get_value(btor, key);
     // Boolector might return the internal name of the variable with a leading BTOR_number@ which we
     // need to strip!
     return new ValueAssignment(

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -104,25 +104,12 @@ public Term makeVariable(Sort sort, String name) {
     if (existingVar != null) {
       return existingVar;
     }
-    if (variablesCache.containsRow(name)) {
-      throw new IllegalArgumentException(
-          "Symbol "
-              + name
-              + " requested with type "
-              + sort
-              + ", but "
-              + "already "
-              + "used "
-              + "with "
-              + "type "
-              + variablesCache
-                  .rowMap()
-                  .get(name)
-                  .entrySet()
-                  .toArray((java.util.Map.Entry[]) Array.newInstance(java.util.Map.Entry.class, 0))[
-                  0]
-                  .getKey());
-    }
+    Preconditions.checkArgument(
+        !variablesCache.containsRow(name),
+        "Symbol %s requested with type %s, but already used with type %s",
+        name,
+        sort,
+        Iterables.getOnlyElement(variablesCache.row(name).entrySet()));
     Term newVar = termManager.mkConst(sort, name);
     variablesCache.put(name, sort.toString(), newVar);
     return newVar;
@@ -860,25 +847,12 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep
 
   private Term accessVariablesCache(String name, Sort sort) {
     Term existingVar = variablesCache.get(name, sort.toString());
-    if (existingVar == null) {
-      throw new IllegalArgumentException(
-          "Symbol "
-              + name
-              + " requested with type "
-              + sort
-              + ", but "
-              + "already "
-              + "used "
-              + "with "
-              + "type"
-              + variablesCache
-                  .rowMap()
-                  .get(name)
-                  .entrySet()
-                  .toArray((java.util.Map.Entry[]) Array.newInstance(java.util.Map.Entry.class, 0))[
-                  0]
-                  .getKey());
-    }
+    Preconditions.checkNotNull(
+        existingVar,
+        "Symbol %s requested with type %s, but already used with type %s",
+        name,
+        sort,
+        Iterables.getOnlyElement(variablesCache.row(name).entrySet()));
     return existingVar;
   }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java

@@ -105,26 +105,7 @@ assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType
     }
 
     // now add the final assert
-    out.append("(assert ");
-    // Formerly in CVC4:
-    // f.toString() does expand all nested sub-expressions and causes exponential overhead.
-    // f.toStream() uses LET-expressions and is exactly what we want.
-    // However, in CVC5 toStream() does no longer exists.
-    // TODO: either toString() will do, or we may need iterator().
-    /*
-    try (OutputStream stream =
-        new OutputStream() {
-
-          @Override
-          public void write(int chr) throws IOException {
-            out.append((char) chr);
-          }
-        }) {
-      f.toStream(stream);
-    }
-    */
-    out.append(f.toString());
-    out.append(')');
+    out.append("(assert ").append(f).append(')');
     return out.toString();
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java

@@ -180,7 +180,7 @@ private ValueAssignment getAssignment(Term pKeyTerm) {
       }
     }
 
-    String nameStr = "";
+    String nameStr;
     if (pKeyTerm.hasSymbol()) {
       nameStr = pKeyTerm.getSymbol();
     } else {

src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java

@@ -27,7 +27,7 @@ public class PrincessRationalFormulaManager
     extends PrincessNumeralFormulaManager<NumeralFormula, RationalFormula>
     implements RationalFormulaManager {
 
-  private PrincessIntegerFormulaManager ifmgr;
+  private final PrincessIntegerFormulaManager ifmgr;
 
   PrincessRationalFormulaManager(
       PrincessFormulaCreator pCreator,