fix Checkstyle warnings about JavaDoc, hidden fields, etc.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/SLFormulaManager.java

@@ -17,11 +17,11 @@
  * complains at runtime!
  *
  * @see <a href="https://en.wikipedia.org/wiki/Separation_logic">Separation Logic</a>
- * @see <a href="https://cacm.acm.org/research/separation-logic/>Separation Logic</a>
+ * @see <a href="https://cacm.acm.org/research/separation-logic/">Separation Logic</a>
  * @see <a
  *     href="https://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15818As2011/cs818A3-11.html">15-818A3
  *     Introduction to Separation Logic (6 units) Spring 2011</a>
- * @see <a href="https://www.philipzucker.com/executable-seperation>Modeling Separation Logic with
+ * @see <a href="https://www.philipzucker.com/executable-seperation">Modeling Separation Logic with
  *     Python Dicts and Z3</a>
  */
 @SuppressWarnings("MethodTypeParameterName")
@@ -52,7 +52,7 @@ public interface SLFormulaManager {
   /**
    * Creates a formula representing the "magic wand" (-*) operator in separation logic. The "magic
    * wand" operator asserts that if the first formula holds, then the second formula can be added to
-   * the heap without conflict. It is a form of implication (=>) that takes into account the
+   * the heap without conflict. It is a form of implication (=&gt;) that takes into account the
    * disjointness of memory regions.
    *
    * @return a Boolean formula representing the "magic wand" of {@code f1} and {@code f2}.

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

@@ -35,7 +35,6 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
-import javax.annotation.Nonnull;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
@@ -55,7 +54,6 @@ abstract class CVC5AbstractProver<T> extends AbstractProverWithAllSat<T> {
   private final FormulaManager mgr;
   protected final CVC5FormulaCreator creator;
   private final int randomSeed;
-  private final ImmutableSet<ProverOptions> options;
   private final ImmutableMap<String, String> furtherOptionsMap;
   protected Solver solver; // final in incremental mode, non-final in non-incremental mode
   private boolean changedSinceLastSatQuery = false;
@@ -79,24 +77,20 @@ protected CVC5AbstractProver(
 
     mgr = pMgr;
     creator = pFormulaCreator;
-    options = ImmutableSet.copyOf(pOptions);
     furtherOptionsMap = pFurtherOptionsMap;
     randomSeed = pRandomSeed;
     incremental = !enableSL;
     assertedTerms.add(PathCopyingPersistentTreeMap.of());
 
     if (incremental) {
-      solver = getNewSolver(randomSeed, options, furtherOptionsMap);
+      solver = getNewSolver();
     }
   }
 
-  protected Solver getNewSolver(
-      int randomSeed,
-      Set<ProverOptions> pOptions,
-      ImmutableMap<String, String> pFurtherOptionsMap) {
+  protected Solver getNewSolver() {
     Solver newSolver = new Solver(creator.getEnv());
     try {
-      CVC5SolverContext.setSolverOptions(newSolver, randomSeed, pFurtherOptionsMap);
+      CVC5SolverContext.setSolverOptions(newSolver, randomSeed, furtherOptionsMap);
     } catch (CVC5ApiRecoverableException e) {
       // We've already used these options in CVC5SolverContext, so there should be no exception
       throw new AssertionError("Unexpected exception", e);
@@ -226,7 +220,7 @@ public boolean isUnsat() throws InterruptedException, SolverException {
       if (solver != null) {
         solver.deletePointer(); // cleanup
       }
-      solver = getNewSolver(randomSeed, options, furtherOptionsMap);
+      solver = getNewSolver();
 
       ImmutableSet<BooleanFormula> assertedFormulas = getAssertedFormulas();
       if (enableSL) {
@@ -237,8 +231,9 @@ public boolean isUnsat() throws InterruptedException, SolverException {
 
     Result result;
     try {
-      result = checkSat();
-    } catch (CVC5ApiException e) {
+      result = solver.checkSat();
+    } catch (Exception e) {
+      // we actually only want to catch CVC5ApiException, but need to catch all.
       throw new SolverException("CVC5 failed during satisfiability check", e);
     } finally {
       /* Shutdown currently not possible in CVC5. */
@@ -247,10 +242,6 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     return convertSatResult(result);
   }
 
-  private Result checkSat() throws CVC5ApiException {
-    return solver.checkSat();
-  }
-
   private void declareHeap(ImmutableSet<BooleanFormula> pAssertedFormulas) throws SolverException {
     // get heap sort from asserted terms
     final Multimap<Sort, Sort> heapSorts;
@@ -278,9 +269,8 @@ private void declareHeap(ImmutableSet<BooleanFormula> pAssertedFormulas) throws
     solver.declareSepHeap(heapSort, elementSort);
   }
 
-  @Nonnull
   private Multimap<Sort, Sort> getHeapSorts(ImmutableSet<BooleanFormula> pAssertedFormulas)
-      throws CVC5ApiException, SolverException {
+      throws CVC5ApiException {
     final Deque<Term> waitlist = new ArrayDeque<>();
     for (BooleanFormula f : pAssertedFormulas) {
       waitlist.add(creator.extractInfo(f));

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

@@ -38,39 +38,30 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver<String>
   private final TermManager termManager = creator.getEnv();
 
   private final FormulaManager mgr;
-  private final Set<ProverOptions> solverOptions;
-  private final ImmutableMap<String, String> furtherOptionsMap;
-  private final int seed;
   private final CVC5BooleanFormulaManager bmgr;
   private final boolean validateInterpolants;
 
   CVC5InterpolatingProver(
       CVC5FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
-      int randomSeed,
+      int pRandomSeed,
       ImmutableSet<ProverOptions> pOptions,
       FormulaManager pMgr,
       ImmutableMap<String, String> pFurtherOptionsMap,
       boolean pValidateInterpolants) {
-    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap);
+    super(pFormulaCreator, pShutdownNotifier, pRandomSeed, pOptions, pMgr, pFurtherOptionsMap);
     mgr = pMgr;
-    solverOptions = pOptions;
-    seed = randomSeed;
     bmgr = (CVC5BooleanFormulaManager) mgr.getBooleanFormulaManager();
     validateInterpolants = pValidateInterpolants;
-    furtherOptionsMap = pFurtherOptionsMap;
   }
 
   /**
    * Sets the same solver Options of the Original Solver to the separate solvertoSet, except for
    * produce-interpolants which is set here. From CVC5AbstractProver Line 66
    */
   @Override
-  protected Solver getNewSolver(
-      int randomSeed,
-      Set<ProverOptions> pOptions,
-      ImmutableMap<String, String> pFurtherOptionsMap) {
-    Solver newSolver = super.getNewSolver(randomSeed, pOptions, pFurtherOptionsMap);
+  protected Solver getNewSolver() {
+    Solver newSolver = super.getNewSolver();
     newSolver.setOption("produce-interpolants", "true");
     return newSolver;
   }
@@ -184,7 +175,7 @@ private Term getCVC5Interpolation(Collection<Term> formulasA, Collection<Term> f
     Term phiMinus = bmgr.andImpl(formulasB);
 
     // Uses a separate Solver instance to leave the original solver-context unmodified
-    Solver itpSolver = getNewSolver(seed, solverOptions, furtherOptionsMap);
+    Solver itpSolver = getNewSolver();
 
     Term interpolant;
     try {
@@ -225,7 +216,7 @@ private void checkInterpolationCriteria(Term interpolant, Term phiPlus, Term phi
 
     // build and check both Craig interpolation formulas with the generated interpolant.
     // interpolation option is not required for validation
-    Solver validationSolver = getNewSolver(seed, solverOptions, furtherOptionsMap);
+    Solver validationSolver = getNewSolver();
     try {
       validationSolver.push();
       validationSolver.assertFormula(termManager.mkTerm(Kind.IMPLIES, phiPlus, interpolant));

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

@@ -24,11 +24,11 @@ class CVC5TheoremProver extends CVC5AbstractProver<Void>
   protected CVC5TheoremProver(
       CVC5FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
-      int randomSeed,
+      int pRandomSeed,
       ImmutableSet<ProverOptions> pOptions,
       FormulaManager pMgr,
       ImmutableMap<String, String> pFurtherOptionsMap) {
-    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap);
+    super(pFormulaCreator, pShutdownNotifier, pRandomSeed, pOptions, pMgr, pFurtherOptionsMap);
   }
 
   @Override