Improve map_representation_of_sum code

Fix typo, avoid double lookup and improve example in the documentation.

Author: romainbrenguier

src/solvers/strings/string_constraint_instantiation.cpp

@@ -52,7 +52,7 @@ find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 
 std::map<exprt, int> map_representation_of_sum(const exprt &f)
 {
-  // number of time the leaf should be added (can be negative)
+  // number of times the leaf should be added (can be negative)
   std::map<exprt, int> elems;
 
   std::list<std::pair<exprt, bool>> to_process;
@@ -80,9 +80,9 @@ std::map<exprt, int> map_representation_of_sum(const exprt &f)
     else
     {
       if(positive)
-        elems[cur] = elems[cur] + 1;
+        ++elems[cur];
       else
-        elems[cur] = elems[cur] - 1;
+        --elems[cur];
     }
   }
   return elems;

src/solvers/strings/string_constraint_instantiation.h

@@ -37,8 +37,8 @@ std::vector<exprt> instantiate_not_contains(
 
 /// \param f: an expression with only addition and subtraction
 /// \return a map where each leaf of the input is mapped to the number of times
-///   it is added. For instance, expression $x + x - y$ would give the map x ->
-///   2, y -> -1.
+///   it is added. For instance, expression $x + x - y + 3 - 5$ would give the
+///   map x -> 2, y -> -1, 3 -> 1, 5 -> -1.
 std::map<exprt, int> map_representation_of_sum(const exprt &f);
 
 /// \param m: a map from expressions to integers