Description: Fix spelling errors found by Lintian
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: https://github.com/CVC4/CVC4/pull/4977
Last-Update: 2020-08-31
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -354,7 +354,7 @@
 ; Helper for `is_operational_drat_proof` which takes a UP model for the working
 ; formula. The UP model is important for determining which clause deletions
 ; actually are executed in operational DRAT. Passing the UP model along
-; prevents it from being fully recomputed everytime.
+; prevents it from being fully recomputed every time.
 (program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool
          (match pf
                 (DRATProofn (cnf_has_bottom f))
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -101,7 +101,7 @@
                                  ((pos v2) ff)
                                  ((neg v2) (ifequal v1 v2 tt ff))))))
 
-; Remove **all** occurences of a literal from clause
+; Remove **all** occurrences of a literal from clause
 (program clause_remove_all ((l lit) (c clause)) clause
          (match c
                 (cln cln)
@@ -180,7 +180,7 @@
                        (CMapc ci c (CMap_remove_many is cs'))))))))
 
 ; Given a map of clauses and a literal, return all indices in the map
-; corresponsing to clauses that could resolve against that literal. i.e. for x,
+; corresponding to clauses that could resolve against that literal. i.e. for x,
 ; return the indices of all clauses containing x.
 (program collect_resolution_targets_w_lit ((cs CMap) (l lit)) CIList
          (match cs
@@ -260,14 +260,14 @@
                                     (fail Unit)
                                     (ifmarked2 v unit (do (markvar2 v) unit))))))
 
-; Unmarks the variable within a satified literal to render it neither satified nor falsified
+; Unmarks the variable within a satisfied literal to render it neither satisfied nor falsified
 ; fails if the literal is not already satisfied
 (program lit_un_mk_sat ((l lit)) Unit
          (match l
                 ((pos v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit)))
                 ((neg v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit)))))
 
-; Unmarks the variable within a falsified literal to render it neither satified nor falsified
+; Unmarks the variable within a falsified literal to render it neither satisfied nor falsified
 ; fails if the literal is not already falsified
 (program lit_un_mk_unsat ((l lit)) Unit
          (match l
@@ -348,7 +348,7 @@
 ; The return type for verifying that a clause is unit and modifying the global
 ; assignment to satisfy it
 (declare MarkResult type)
-; The clause is unit, and this is the (previoiusly floating) literal that is now satified.
+; The clause is unit, and this is the (previoiusly floating) literal that is now satisfied.
 (declare MRUnit (! l lit MarkResult))
 ; The clause was unsat!
 (declare MRUnsat MarkResult)
@@ -357,7 +357,7 @@
 ; The clause had multiple floating literals.
 (declare MRNotUnit MarkResult)
 
-; Determine wether this clause is sat, unsat, unit, or not unit, and if it is
+; Determine whether this clause is sat, unsat, unit, or not unit, and if it is
 ; unit, it modifies the global assignment to satisfy the clause, and returns
 ; the literal that was made SAT by the new mark.
 ;
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2684,10 +2684,10 @@
   CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
                      == std::string::npos
                  && s.size() <= 5 && s.size() > 0)
-      << "Unexpected string for hexidecimal character " << s;
+      << "Unexpected string for hexadecimal character " << s;
   uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
   CVC4_API_CHECK(val < String::num_codes())
-      << "Not a valid code point for hexidecimal character " << s;
+      << "Not a valid code point for hexadecimal character " << s;
   std::vector<unsigned> cpts;
   cpts.push_back(val);
   return mkValHelper<CVC4::String>(CVC4::String(cpts));
@@ -5042,7 +5042,7 @@
 
   std::map<CVC4::Expr, CVC4::Expr> map;
   CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map))
-      << "The solver is not in a state immediately preceeded by a "
+      << "The solver is not in a state immediately preceded by a "
          "successful call to checkSynth";
 
   std::map<CVC4::Expr, CVC4::Expr>::const_iterator it = map.find(*term.d_expr);
@@ -5071,7 +5071,7 @@
 
   std::map<CVC4::Expr, CVC4::Expr> map;
   CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map))
-      << "The solver is not in a state immediately preceeded by a "
+      << "The solver is not in a state immediately preceded by a "
          "successful call to checkSynth";
 
   std::vector<Term> synthSolution;
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2488,7 +2488,7 @@
 fragment DOTDOT:;
 
 /**
- * Matches the hexidecimal digits (0-9, a-f, A-F)
+ * Matches the hexadecimal digits (0-9, a-f, A-F)
  */
 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
 
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4763,7 +4763,7 @@
     //We are only going to recreate the functionality for now.
     //In the future this can be improved to generate a temporary constraint
     //if none exists.
-    //Experiment with doing this everytime or only when the new constraint
+    //Experiment with doing this every time or only when the new constraint
     //implies an unknown fact.
 
     ConstraintType t = upperBound ? UpperBound : LowerBound;
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -131,7 +131,7 @@
     ++i;
     // are we an escape sequence?
     bool isEscapeSequence = true;
-    // the string corresponding to the hexidecimal code point
+    // the string corresponding to the hexadecimal code point
     std::stringstream hexString;
     // is the slash followed by a 'u'? Could be last character.
     if (i >= s.size() || s[i] != 'u')
@@ -195,7 +195,7 @@
       }
       if (!isEnd)
       {
-        // if we were interupted before ending, then this is not a valid
+        // if we were interrupted before ending, then this is not a valid
         // escape sequence
         isEscapeSequence = false;
       }
@@ -210,7 +210,7 @@
       if (val > num_codes())
       {
         // Failed due to being out of range. This can happen for strings of
-        // the form \ u { d_4 d_3 d_2 d_1 d_0 } where d_4 is a hexidecimal not
+        // the form \ u { d_4 d_3 d_2 d_1 d_0 } where d_4 is a hexadecimal not
         // in the range [0-2].
         isEscapeSequence = false;
       }
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -58,7 +58,7 @@
    *  \u{d_2 d_1 d_0}
    *  \u{d_3 d_2 d_1 d_0}
    *  \u{d_4 d_3 d_2 d_1 d_0}
-   * where d_0 ... d_4 are hexidecimal digits, to the appropriate character.
+   * where d_0 ... d_4 are hexadecimal digits, to the appropriate character.
    *
    * If useEscSequences is false, then the characters of the constructed
    * CVC4::String correspond one-to-one with the input string.
@@ -211,7 +211,7 @@
    * This is true for code points between 48 ('0') and 57 ('9').
    */
   static bool isDigit(unsigned character);
-  /** is the unsigned a hexidecimal digit?
+  /** is the unsigned a hexadecimal digit?
    *
    * This is true for code points between 48 ('0') and 57 ('9'), code points
    * between 65 ('A') and 70 ('F) and code points between 97 ('a') and 102 ('f).
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -128,7 +128,7 @@
     (default (fail (term Int)))
   ))
 
-; This function negates linear interger terms---sums of terms of the form
+; This function negates linear integer terms---sums of terms of the form
 ; recognized by `negate_linear_monomial_int_term`.
 (program negate_linear_int_term ((t (term Int))) (term Int)
   (match t
@@ -339,7 +339,7 @@
 ; the statement that `a` satisfies `b` for all inputs
 (declare bounded_aff (! a aff (! b bound formula)))
 
-; Sum of two bounds (the bound satisfied by the sum of two functions satifying
+; Sum of two bounds (the bound satisfied by the sum of two functions satisfying
 ; the input bounds)
 (program bound_add ((b bound) (b2 bound)) bound
   (match b
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1450,7 +1450,7 @@
     std::stringstream ss;
     ss << "Cannot " << c
        << " since model is not available. Perhaps the most recent call to "
-          "check-sat was interupted?";
+          "check-sat was interrupted?";
     throw RecoverableModalException(ss.str().c_str());
   }
 
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -582,7 +582,7 @@
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
-    //flush previous lemmas (for instance, if was interupted), or other lemmas to process
+    //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
     flushLemmas();
     if( d_hasAddedLemma ){
       return;
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -54,7 +54,7 @@
                  Lit r,
                  ClauseId& id);  // Add a ternary clause to the solver.
   bool addClause_(vec<Lit>& ps, ClauseId& id);
-  bool substitute(Var v, Lit x);  // Replace all occurences of v with x (may
+  bool substitute(Var v, Lit x);  // Replace all occurrences of v with x (may
                                   // cause a contradiction).
 
   // Variable mode:
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -55,7 +55,7 @@
     bool    addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver.
     bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
     bool    addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
-    bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
+    bool    substitute(Var v, Lit x);  // Replace all occurrences of v with x (may cause a contradiction).
 
     // Variable mode:
     // 
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -562,7 +562,7 @@
   /**
    * Get synth solution.
    *
-   * This method returns true if we are in a state immediately preceeded by
+   * This method returns true if we are in a state immediately preceded by
    * a successful call to checkSynth.
    *
    * This method adds entries to sol_map that map functions-to-synthesize with
--- a/src/theory/example/ecdata.h
+++ b/src/theory/example/ecdata.h
@@ -165,7 +165,7 @@
    * Pointer to the end of the watch-list.
    * This is maintained in order to constant time list merging.
    * (This does not give any asymptotic improve as this is currently always
-   * preceeded by an O(|watchlist|) operation.)
+   * preceded by an O(|watchlist|) operation.)
    * This value is NULL iff the watch list is empty.
    */
   Link* d_last;
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -538,7 +538,7 @@
     for (int i = 0; i < cls.size(); i++)
         (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
 
-    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+    // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
     // clause must exceed the limit on the maximal clause size (if it is set):
     //
     int cnt         = 0;
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -525,7 +525,7 @@
     for (int i = 0; i < cls.size(); i++)
         (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
 
-    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+    // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
     // clause must exceed the limit on the maximal clause size (if it is set):
     //
     int cnt         = 0;
--- a/src/theory/example/theory_uf_tim.h
+++ b/src/theory/example/theory_uf_tim.h
@@ -163,7 +163,7 @@
   bool equiv(TNode x, TNode y);
 
   /**
-   * Merges 2 equivalence classes, checks wether any predecessors need to
+   * Merges 2 equivalence classes, checks whether any predecessors need to
    * be set equal to complete congruence closure.
    * The class with the smaller class size will be merged.
    * @pre ecX->isClassRep()