Merge pull request #1479 from waywardmonkeys/fix-more-typos

Fix typos.

src/ast/rewriter/der.cpp

@@ -260,7 +260,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
                 vidx = to_var(t)->get_idx();
                 if (fr.second == 0) {
                     CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
-                    // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
+                    // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
                     if (definitions.get(vidx, 0) != 0) {
                         if (visiting.is_marked(t)) {
                             // cycle detected: remove t

src/duality/duality.h

@@ -722,7 +722,7 @@ namespace Duality {
 
         check_result CheckUpdateModel(Node *root, std::vector<expr> assumps);
 
-        /** Determines the value in the counterexample of a symbol occuring in the transformer formula of
+        /** Determines the value in the counterexample of a symbol occurring in the transformer formula of
          *  a given edge. */
 
         Term Eval(Edge *e, Term t);
@@ -731,7 +731,7 @@ namespace Duality {
 
         Term EvalNode(Node *p);
 
-        /** Returns true if the given node is empty in the primal solution. For proecudure summaries,
+        /** Returns true if the given node is empty in the primal solution. For procedure summaries,
             this means that the procedure is not called in the current counter-model. */
 
         bool Empty(Node *p);
@@ -854,7 +854,7 @@ namespace Duality {
         /** Write the RPFP to a file (currently in SMTLIB 1.2 format) */
         void WriteProblemToFile(std::string filename, FileFormat format = DualityFormat);
 
-        /** Read the RPFP from a file (in specificed format) */
+        /** Read the RPFP from a file (in specified format) */
         void ReadProblemFromFile(std::string filename, FileFormat format = DualityFormat);
 
         /** Translate problem to Horn clause form */
@@ -870,9 +870,9 @@ namespace Duality {
         std::vector<Edge *> edges;
 
         /** Fuse a vector of transformers. If the total number of inputs of the transformers
-            is N, then the result is an N-ary transfomer whose output is the union of
+            is N, then the result is an N-ary transformer whose output is the union of
-            the outputs of the given transformers. The is, suppose we have a vetor of transfoermers
+            the outputs of the given transformers. The is, suppose we have a vector of transformers
-            {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer
+            {T_i(r_i1,...,r_iN(i) : i=1..M}. The result is a transformer
 
             F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) =
             T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M))

src/duality/duality_rpfp.cpp

@@ -1491,7 +1491,7 @@ namespace Duality {
         return res;
     }      
 
-    /** Determines the value in the counterexample of a symbol occuring in the transformer formula of
+    /** Determines the value in the counterexample of a symbol occurring in the transformer formula of
      *  a given edge. */
 
     RPFP::Term RPFP::Eval(Edge *e, Term t)
@@ -1500,7 +1500,7 @@ namespace Duality {
         return dualModel.eval(tl);
     }
 
-    /** Returns true if the given node is empty in the primal solution. For proecudure summaries,
+    /** Returns true if the given node is empty in the primal solution. For proceudure summaries,
         this means that the procedure is not called in the current counter-model. */
   
     bool RPFP::Empty(Node *p)

src/math/polynomial/polynomial.cpp

@@ -1421,7 +1421,7 @@ namespace polynomial {
             }
         }
 
-        // Return the maximal variable y occuring in [m_ms + start, m_ms + end) that is smaller than x
+        // Return the maximal variable y occurring in [m_ms + start, m_ms + end) that is smaller than x
         var max_smaller_than(unsigned start, unsigned end, var x) {
             var max = null_var;
             for (unsigned i = start; i < end; i++) {
@@ -1456,7 +1456,7 @@ namespace polynomial {
         }
 
         /**
-           \brief Make sure that the first monomial contains the maximal variable x occuring in the polynomial,
+           \brief Make sure that the first monomial contains the maximal variable x occurring in the polynomial,
            and x occurs with maximal degree.
         */
         void make_first_maximal() {
@@ -3209,7 +3209,7 @@ namespace polynomial {
         typedef sbuffer<var, 32>      var_buffer;
 
         /**
-           Store in pws the variables occuring in p and their (minimal or maximal) degrees.
+           Store in pws the variables occurring in p and their (minimal or maximal) degrees.
         */
         unsigned_vector m_var_degrees_tmp;
         template<bool Max>
@@ -3470,7 +3470,7 @@ namespace polynomial {
                 pp = mk_one();
                 return;
             }
-            // Apply filter and collect powers of x occuring in p
+            // Apply filter and collect powers of x occurring in p
             // The quick filter is the following:
             //   If p contains a monomial x^k and no monomial of the form m*x^k m != 1, then
             //      c = m_unit_poly
@@ -3479,7 +3479,7 @@ namespace polynomial {
             //      - found monomial x^k then iccp_powers[k]++;
             //      - found monomial m*x^k then iccp_powers[k]+=2;
             //   If after traversing p, there is a k s.t. iccp_powers[k] == 1, we know c == 1
-            // We store iccp_powers the powers of x occuring in p.
+            // We store iccp_powers the powers of x occurring in p.
             sbuffer<unsigned, 128> iccp_filter;
             sbuffer<unsigned, 128> iccp_powers;
             iccp_filter.resize(d+1, 0);

src/muz/spacer/spacer_unsat_core_learner.cpp

@@ -46,7 +46,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
            verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";
     );
 
-    // compute symbols occuring in B
+    // compute symbols occurring in B
     collect_symbols_b(asserted_b);
 
     // traverse proof

src/qe/qe_lite.cpp

@@ -125,7 +125,7 @@ namespace eq {
                         vidx = to_var(t)->get_idx();
                         if (fr.second == 0) {
                             CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
-                            // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
+                            // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
                             if (definitions.get(vidx, 0) != 0) {
                                 if (visiting.is_marked(t)) {
                                     // cycle detected: remove t

src/smt/theory_arith_core.h

@@ -40,7 +40,7 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
         if (!m_found_underspecified_op) {
-            TRACE("arith", tout << "found underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
+            TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";);
             get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
             m_found_underspecified_op = true;
         }

src/smt/theory_arith_nl.h

@@ -141,8 +141,8 @@ namespace smt {
        \brief Return the number of variables that
        do not have bounds associated with it.
        The result is 0, 1, or 2. The value 2 means "2 or more".
-       The second value is the idx of the a variable that does not
+       The second value is the idx of the variable that does not
-       have bounds associated with it. It is only usefull when the first value is 1.
+       have bounds associated with it. It is only useful when the first value is 1.
        The second value is -1 if such variable does not exist, that is, the first
        value is 0.
 

src/tactic/arith/fix_dl_var_tactic.cpp

@@ -196,7 +196,7 @@ class fix_dl_var_tactic : public tactic {
 
         app * most_occs() {
             // We try to choose a variable that when set to 0 will generate many bounded variables.
-            // That is why we give preference to variables occuring in non-nested inequalities.
+            // That is why we give preference to variables occurring in non-nested inequalities.
             unsigned best1, best2;
             app * r1, * r2;
             r1 = most_occs(m_non_nested_occs, best1);

src/tactic/core/occf_tactic.cpp

@@ -9,7 +9,7 @@ Abstract:
 
     Put clauses in the assertion set in
     OOC (one constraint per clause) form.
-    Constraints occuring in formulas that
+    Constraints occurring in formulas that
     are not clauses are ignored.
     The formula can be put into CNF by
     using mk_sat_preprocessor strategy.

src/tactic/core/occf_tactic.h

@@ -9,7 +9,7 @@ Abstract:
 
     Put clauses in the assertion set in
     OOC (one constraint per clause) form.
-    Constraints occuring in formulas that
+    Constraints occurring in formulas that
     are not clauses are ignored.
     The formula can be put into CNF by
     using mk_sat_preprocessor strategy.