apply a spell check for documentation and comments in source code.

Author: kfriedberger

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -121,7 +121,7 @@ public SolverContextFactory(
 
   /**
    * This constructor instantiates a factory for building solver contexts for a configured SMT
-   * solver (via the parameter <code>pConfig</code>). Each created context is independent from other
+   * solver (via the parameter <code>pConfig</code>). Each created context is independent of other
    * contexts and uses its own environment for building formulas and querying the solver.
    *
    * @param pConfig The configuration to be used when instantiating JavaSMT and the solvers. By

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

@@ -62,7 +62,7 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
   /**
    * Get a satisfying assignment. This should be called only immediately after an {@link #isUnsat()}
    * call that returned <code>false</code>. A model might contain additional symbols with their
-   * evaluation, if a solver uses its own temporary symbols. There should be at least an
+   * evaluation, if a solver uses its own temporary symbols. There should be at least a
    * value-assignment for each free symbol.
    */
   Model getModel() throws SolverException;
@@ -106,8 +106,8 @@ Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormul
   void close();
 
   /**
-   * Get all satisfying assignments of the current environment with regards to a subset of terms,
-   * and create a region representing all those models.
+   * Get all satisfying assignments of the current environment with regard to a subset of terms, and
+   * create a region representing all those models.
    *
    * @param important A set of (positive) variables appearing in the asserted queries. Only these
    *     variables will appear in the region.
@@ -129,12 +129,12 @@ interface AllSatCallback<R> {
      * otherwise it is negated.
      *
      * <p>There is no guarantee that the list of model values corresponds to the list in {@link
-     * BasicProverEnvironment#allSat}. We can reorder the variables or leave out values with an
+     * BasicProverEnvironment#allSat}. We can reorder the variables or leave out values with a
      * freely chosen value.
      */
     void apply(List<BooleanFormula> model);
 
-    /** Returning the result generated after all the {@link #apply} calls have went through. */
+    /** Returning the result generated after all the {@link #apply} calls went through. */
     R getResult() throws InterruptedException;
   }
 }

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

@@ -125,9 +125,9 @@ BooleanFormula greaterOrEquals(
 
   /**
    * @param number The bitvector to extract.
-   * @param msb Upper index. Must be greater then or equal to 0 and less then the bit-width of
+   * @param msb Upper index. Must be greater than or equal to 0 and less than the bit-width of
    *     number.
-   * @param lsb Lower index. Must be less then or equal to msb and greater or equal to 0.
+   * @param lsb Lower index. Must be less than or equal to msb and greater or equal to 0.
    * @param signed Whether the extension should depend on the sign bit. Note: Some SMT-Solvers
    *     ignore this. (i.e. Boolector)
    */

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

@@ -142,7 +142,7 @@ default BooleanFormula makeBoolean(boolean value) {
    * and thus is not prone to StackOverflowErrors.
    *
    * <p>Furthermore, this method also guarantees that every equal part of the formula is visited
-   * only once. Thus it can be used to traverse DAG-like formulas efficiently.
+   * only once. Thus, it can be used to traverse DAG-like formulas efficiently.
    */
   void visitRecursively(BooleanFormula f, BooleanFormulaVisitor<TraversalProcess> rFormulaVisitor);
 
@@ -154,7 +154,7 @@ default BooleanFormula makeBoolean(boolean value) {
    * and thus is not prone to StackOverflowErrors.
    *
    * <p>Furthermore, this method also guarantees that every equal part of the formula is visited
-   * only once. Thus it can be used to traverse DAG-like formulas efficiently.
+   * only once. Thus, it can be used to traverse DAG-like formulas efficiently.
    */
   BooleanFormula transformRecursively(
       BooleanFormula f, BooleanFormulaTransformationVisitor pVisitor);

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

@@ -76,7 +76,7 @@ <T extends Formula> T castTo(
    *
    * @param source the source formula of compatible type
    * @param signed if a {@link BitvectorFormula} is given as source, we additionally use this flag.
-   *     Otherwise we ignore it.
+   *     Otherwise, we ignore it.
    * @param targetType the type of the resulting formula
    * @throws IllegalArgumentException if an incompatible type is used, e.g. a {@link BooleanFormula}
    *     cannot be cast to {@link FloatingPointFormula}.
@@ -93,7 +93,7 @@ <T extends Formula> T castTo(
    *
    * @param source the source formula of compatible type
    * @param signed if a {@link BitvectorFormula} is given as source, we additionally use this flag.
-   *     Otherwise we ignore it.
+   *     Otherwise, we ignore it.
    * @param targetType the type of the resulting formula
    * @param pFloatingPointRoundingMode if rounding is needed, we apply the rounding mode.
    * @throws IllegalArgumentException if an incompatible type is used, e.g. a {@link BooleanFormula}

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

@@ -20,7 +20,7 @@ public interface Formula {
    *
    * <p>We do not guarantee that the returned String is in any way related to the formula. The
    * solver might apply escaping or even un-escaping. A user should not use the returned String for
-   * further processing. For analyzing formulas, we recommend to use a {@link FormulaVisitor}.
+   * further processing. For analyzing formulas, we recommend using a {@link FormulaVisitor}.
    */
   @Override
   String toString();

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

@@ -167,7 +167,7 @@ <T extends Formula> T makeApplication(
    *
    * <p>Please be aware that calling this method might cause extensive stack usage depending on the
    * nesting of the given formula and the given {@link FormulaVisitor}. Additionally, sub-formulas
-   * that are used several times in the formula might be visited several times. For a efficient
+   * that are used several times in the formula might be visited several times. For an efficient
    * formula traversing, we also provide {@link #visitRecursively(Formula, FormulaVisitor)}.
    *
    * @param f formula to be visited
@@ -185,7 +185,7 @@ <T extends Formula> T makeApplication(
    * and thus is not prone to StackOverflowErrors.
    *
    * <p>Furthermore, this method also guarantees that every equal part of the formula is visited
-   * only once. Thus it can be used to traverse DAG-like formulas efficiently.
+   * only once. Thus, it can be used to traverse DAG-like formulas efficiently.
    */
   void visitRecursively(Formula f, FormulaVisitor<TraversalProcess> rFormulaVisitor);
 
@@ -196,7 +196,7 @@ <T extends Formula> T makeApplication(
    * and thus is not prone to StackOverflowErrors.
    *
    * <p>Furthermore, this method also guarantees that every equal part of the formula is visited
-   * only once. Thus it can be used to traverse DAG-like formulas efficiently.
+   * only once. Thus, it can be used to traverse DAG-like formulas efficiently.
    *
    * @param pFormulaVisitor Transformation described by the user.
    */
@@ -253,10 +253,10 @@ <T extends Formula> T makeApplication(
    * possible not use logical or mathematical operators, or keywords strongly depending on SMTlib.
    *
    * <p>If a variable name is rejected, a possibility is escaping, e.g. either substituting the
-   * whole variable name or just every invalid character with an escaped form. We recommend to use
-   * an escape sequence based on the token "JAVASMT", because it might be unusual enough to appear
-   * when encoding a user's problem in SMT. Please not that you might also have to handle escaping
-   * the escape sequence. Examples:
+   * whole variable name or just every invalid character with an escaped form. We recommend using an
+   * escape sequence based on the token "JAVASMT", because it might be unusual enough to appear when
+   * encoding a user's problem in SMT. Please note that you might also have to handle escaping the
+   * escape sequence. Examples:
    *
    * <ul>
    *   <li>the invalid variable name <code>"="</code> (logical operator for equality) can be

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

@@ -53,7 +53,7 @@ public interface Model extends Iterable<ValueAssignment>, AutoCloseable {
    *
    * @param f Input formula
    * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
-   * @throws IllegalArgumentException if a formula has unexpected type, e.g Array.
+   * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array.
    */
   @Nullable
   Object evaluate(Formula f);
@@ -123,7 +123,7 @@ final class ValueAssignment {
      *
      * <p>For arrays we use the selection-statement with an index. We do not support Array theory as
      * {@link #value} during a model evaluation, but we provide assignments like <code>
-     * select(arr, 12) := 34</code> (where <code>arr</code> itself is a plain symbol (without an
+     * select(arr, 12) := 34</code> where <code>arr</code> itself is a plain symbol (without an
      * explicit const- or zero-based initialization, as done by some SMT solvers).
      */
     private final Formula keyFormula;

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

@@ -64,7 +64,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    * (epsilon can even be set to zero). The model can return the assignment x=9. To get an optimal
    * assignment, query the solver with an additional constraint 'x == 10-epsilon'.
    *
-   * <p>Example 2: For the constraint 'x&lt;10' with a integer x, the upper bound of x is '9'
+   * <p>Example 2: For the constraint 'x&lt;10' with an integer x, the upper bound of x is '9'
    * (epsilon is irrelevant here and can be zero). The model returns the optimal assignment x=9.
    */
   @Override

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

@@ -19,6 +19,6 @@
  * <p>All solving methods are expected to throw {@link SolverException} if the solver fails to solve
  * the given query, and {@link InterruptedException} if a thread interrupt was requested or a
  * shutdown request via the {@link ShutdownNotifier}. It is not guaranteed, though, that solvers
- * respond in a timely manner (or at all) to shutdown or interrupt requests.
+ * respond in a timely manner (or at all) to shut down or interrupt requests.
  */
 public interface ProverEnvironment extends BasicProverEnvironment<Void> {}

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

@@ -59,27 +59,27 @@ enum ProverOptions {
    * Create a fresh new {@link ProverEnvironment} which encapsulates an assertion stack and can be
    * used to check formulas for unsatisfiability.
    *
-   * @param options Options specified for the prover environment. All of the options specified in
+   * @param options Options specified for the prover environment. All the options specified in
    *     {@link ProverOptions} are turned off by default.
    */
   ProverEnvironment newProverEnvironment(ProverOptions... options);
 
   /**
    * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack
-   * and allows to generate and retrieve interpolants for unsatisfiable formulas. If the SMT solver
+   * and allows generating and retrieve interpolants for unsatisfiable formulas. If the SMT solver
    * is able to handle satisfiability tests with assumptions please consider implementing the {@link
    * InterpolatingProverEnvironment} interface, and return an Object of this type here.
    *
-   * @param options Options specified for the prover environment. All of the options specified in
+   * @param options Options specified for the prover environment. All the options specified in
    *     {@link ProverOptions} are turned off by default.
    */
   InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(ProverOptions... options);
 
   /**
    * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack
-   * and allows to solve optimization queries.
+   * and allows solving optimization queries.
    *
-   * @param options Options specified for the prover environment. All of the options specified in
+   * @param options Options specified for the prover environment. All the options specified in
    *     {@link ProverOptions} are turned off by default.
    */
   OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options);
@@ -103,9 +103,9 @@ enum ProverOptions {
    * Close the solver context.
    *
    * <p>After calling this method, further access to any object that had been returned from this
-   * context is not wanted, i.e., it is depending on the solver. Java-based solvers might wait for
-   * the next garbage collection with any cleanup operation. Native solvers might even reference
-   * invalid memory and cause segmentation faults.
+   * context is not wanted, i.e., it depends on the solver. Java-based solvers might wait for the
+   * next garbage collection with any cleanup operation. Native solvers might even reference invalid
+   * memory and cause segmentation faults.
    *
    * <p>Necessary for the solvers implemented in native code, frees the associated memory.
    */

src/org/sosy_lab/java_smt/api/visitors/FormulaVisitor.java

@@ -50,7 +50,7 @@ public interface FormulaVisitor<R> {
    * @param f Formula representing the constant.
    * @param value The value of the constant. It is either of type {@link Boolean} or of a subtype of
    *     {@link Number}, mostly a {@link BigInteger}, a {@link BigDecimal}, or a {@link Rational}.
-   * @return An arbitrary return value that is be passed to the caller.
+   * @return An arbitrary return value that is passed to the caller.
    */
   R visitConstant(Formula f, Object value);
 

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

@@ -88,7 +88,7 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
 
   /** Mapping of disallowed char to their escaped counterparts. */
   /* Keep this map in sync with {@link #DISALLOWED_CHARACTERS}.
-   * Counterparts can be any unique string. For optimization we could even use plain chars. */
+   * Counterparts can be any unique string. For optimization, we could even use plain chars. */
   @VisibleForTesting
   public static final ImmutableBiMap<Character, String> DISALLOWED_CHARACTER_REPLACEMENT =
       ImmutableBiMap.<Character, String>builder().put('|', "pipe").put('\\', "backslash").build();

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

@@ -22,7 +22,7 @@
 import org.sosy_lab.java_smt.api.SolverException;
 
 /**
- * This class is an utility-class to avoid repeated implementation of a the AllSAT computation.
+ * This class is a utility-class to avoid repeated implementation of the AllSAT computation.
  *
  * <p>If a solver does not support direct AllSAT computation, please inherit from this class.
  */
@@ -100,7 +100,7 @@ private <R> void iterateOverAllModels(
 
   /**
    * This method computes all satisfiable assignments for the given predicates by (recursively)
-   * traversing the decision tree over the given variables. The ordering of variables is fixed and
+   * traversing the decision tree over the given variables. The ordering of variables is fixed, and
    * we can only ignore unsatisfiable subtrees.
    *
    * <p>In contrast to {@link #iterateOverAllModels} we do not use model generation here, which is a

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

@@ -87,7 +87,7 @@ protected abstract OptimizationProverEnvironment newOptimizationProverEnvironmen
    * methods. This class will wrap the prover environments and provide an implementation of the
    * feature.
    *
-   * <p>This method is expected to always return the same value. Otherwise the behavior of this
+   * <p>This method is expected to always return the same value. Otherwise, the behavior of this
    * class is undefined.
    */
   protected abstract boolean supportsAssumptionSolving();
@@ -105,15 +105,15 @@ private static Set<ProverOptions> toSet(ProverOptions... options) {
    * two lists of libraries can be used to differ between libraries specific to Unix/Linux and
    * Windows.
    *
-   * <p>If the first try a aborts after a few steps, we do not cleanup partially loaded libraries,
+   * <p>If the first try aborts after a few steps, we do not clean up partially loaded libraries,
    * but directly start the second try.
    *
    * <p>Each list is applied in the given ordering.
    *
    * @param loader the loading mechanism that will be used for loading each single library.
    * @param librariesForFirstTry list of library names that will be loaded, if possible.
    * @param librariesForSecondTry list of library names that will be loaded, after the first attempt
-   *     (using librariesForFirstTry} has failed.
+   *     (using librariesForFirstTry) has failed.
    * @throws UnsatisfiedLinkError if neither the first nor second try returned a successful loading
    *     process.
    */

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

@@ -403,7 +403,7 @@ public TFuncDecl getBooleanVarDeclaration(BooleanFormula var) {
    * Convert the formula into a Java object as far as possible, i.e., try to match a primitive or
    * simple type like Boolean, BigInteger, or Rational.
    *
-   * <p>If the formula is not a simple constant expression, we simple return <code>null</code>.
+   * <p>If the formula is not a simple constant expression, we simply return <code>null</code>.
    *
    * @param pF the formula to be converted.
    */

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

@@ -82,8 +82,7 @@ public Void visitFunction(
     // of the function were already processed.
     if (allArgumentsTransformed) {
 
-      // Create an processed version of the
-      // function application.
+      // Create a processed version of the function application.
       if (!toProcess.isEmpty()) {
         toProcess.pop();
       }

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

@@ -41,7 +41,7 @@ public void shutdownRequested(@Nullable String reasonUnused) {
     while (isActiveHook.get()) { // flag is reset in #cancelHook
       interruptCall.run();
       try {
-        Thread.sleep(10); // lets wait a few steps
+        Thread.sleep(10); // let's wait a few steps
       } catch (InterruptedException e) {
         // ignore
       }

src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java

@@ -10,7 +10,7 @@
  * Wrapper-classes to guarantee identical behavior for all solvers. If a solver does not support
  * {@link org.sosy_lab.java_smt.api.BasicProverEnvironment#isUnsatWithAssumptions}, we wrap it in a
  * (subclass of) BasicProverWithAssumptionsWrapper, whose task it is to keep the assumptions as long
- * on the solver's stack as no other operation accesses it. It allows to compute interpolants and
+ * on the solver's stack as no other operation accesses it. It allows computing interpolants and
  * unsat cores. without direct support from the solver.
  */
 package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper;

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

@@ -140,7 +140,7 @@ private static void printUpperAndLowerBound(
     prover.pop();
 
     prover.push();
-    { // maximize x and get a upper bound of x: x < 10
+    { // maximize x and get an upper bound of x: x < 10
       // --> bound is (10 - EPSILON) for rational symbols and 9 for integer symbols.
       int handleX = prover.maximize(x);
       OptStatus status = prover.check();

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

@@ -204,7 +204,7 @@ public static class SolverInfo {
     private final String solverFeatures;
 
     /**
-     * Saves the information of an solver.
+     * Saves the information of a solver.
      *
      * @param solver Solvers enum object for a solver.
      * @param solverVersion Solver version String.

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

@@ -34,7 +34,7 @@
 
 public class BoolectorFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
 
-  // Boolector can give back 'x' for a arbitrary value that we change to this
+  // Boolector can give back 'x' for an arbitrary value that we change to this
   private static final char ARBITRARY_VALUE = '1';
 
   /** Maps a name and a variable or function type to a concrete formula node. */
@@ -164,8 +164,8 @@ public Long makeVariable(Long type, String varName) {
     return newVar;
   }
 
-  // This method is a massive problem... you CANT get the value formulas(nodes) because they are
-  // only build and used internally in boolector. (See visit1 for help)
+  // This method is a massive problem... you CAN'T get the value formulas(nodes) because they are
+  // only build and used internally in Boolector. (See visit1 for help)
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Long f) {
     throw new UnsupportedOperationException(