fix typos in goto-synthesizer

Author: qinheping

src/goto-synthesizer/dump_loop_contracts.cpp

@@ -91,16 +91,16 @@ void dump_loop_contracts(
         "loop " + std::to_string(invariant_entry.first.loop_number + 1) +
         " assigns ";
 
-      bool in_fisrt_iter = true;
+      bool in_first_iter = true;
       for(const auto &a : it_assigns->second)
       {
-        if(!in_fisrt_iter)
+        if(!in_first_iter)
         {
           assign_string += ",";
         }
         else
         {
-          in_fisrt_iter = false;
+          in_first_iter = false;
         }
         assign_string += expr2c(
           simplify_expr(a, ns), ns, expr2c_configurationt::clean_configuration);

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h

@@ -53,7 +53,7 @@ class enumerative_loop_contracts_synthesizert
   /// to their original variables.
   void build_tmp_post_map();
 
-  /// Compute the depedent symbols for a loop with invariant-not-preserved
+  /// Compute the dependent symbols for a loop with invariant-not-preserved
   /// violation which happen after `new_clause` was added.
   std::set<symbol_exprt> compute_dependent_symbols(
     const loop_idt &cause_loop_id,

src/goto-synthesizer/expr_enumerator.cpp

@@ -208,7 +208,7 @@ std::vector<std::size_t> get_ones_pos(std::size_t v)
   return result;
 }
 
-/// Construct parition of `n` elements from a bit vector `v`.
+/// Construct partition of `n` elements from a bit vector `v`.
 /// For a bit vector with ones at positions (computed by `get_ones_pos`)
 /// (ones[0], ones[1], ..., ones[k-2]),
 /// the corresponding partition is
@@ -255,7 +255,7 @@ std::list<partitiont> non_leaf_enumeratort::get_partitions(
 
   // Initial `v` is with ones at positions (n-k+1, n-k+2, ..., n-2, n-1).
   std::size_t v = 0;
-  // Initial `end` (the last bit vectorr we enumerate) is with ones at
+  // Initial `end` (the last bit vector we enumerate) is with ones at
   // positions (1, 2, 3, ..., k-1).
   std::size_t end = 0;
   for(size_t i = 0; i < k - 1; i++)
@@ -412,5 +412,5 @@ void enumerator_factoryt::attach_productions(
 {
   const auto &ret = productions_map.insert({id, enumerators});
   INVARIANT(
-    ret.second, "Cannnot attach enumerators to a non-existing nonterminal.");
+    ret.second, "Cannot attach enumerators to a non-existing nonterminal.");
 }

src/goto-synthesizer/expr_enumerator.h

@@ -158,7 +158,7 @@ class non_leaf_enumeratort : public enumerator_baset
   /// enumerated by the enumerator e_i.
   /// \param partition_check an optional function checking whether a partition
   /// can be safely discarded.
-  /// \param ns namesapce used by `simplify_expr`.
+  /// \param ns namespace used by `simplify_expr`.
   non_leaf_enumeratort(
     const enumeratorst &enumerators,
     const std::function<bool(const partitiont &)> partition_check,
@@ -337,7 +337,7 @@ class recursive_enumerator_placeholdert : public enumerator_baset
   /// \param factory the enumerator factory---a grammar---this enumerator
   /// belongs to.
   /// \param id the identifier of this placeholder.
-  /// \param ns namesapce used for `simplify_expr`.
+  /// \param ns namespace used for `simplify_expr`.
   recursive_enumerator_placeholdert(
     enumerator_factoryt &factory,
     const std::string &id,