Don't mutate parameters in numbering class

Author: reuk

src/analyses/invariant_set.cpp

@@ -52,7 +52,12 @@ bool inv_object_storet::get(const exprt &expr, unsigned &n)
     return false;
   }
 
-  return map.get_number(s, n);
+  if(const auto number = map.get_number(s))
+  {
+    n = *number;
+    return false;
+  }
+  return true;
 }
 
 unsigned inv_object_storet::add(const exprt &expr)

src/solvers/flattening/boolbv_get.cpp

@@ -330,13 +330,14 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
   valuest values;
 
   {
-    std::size_t number;
-
-    if(arrays.get_number(expr, number))
+    const auto opt_num = arrays.get_number(expr);
+    if(!opt_num)
+    {
       return nil_exprt();
+    }
 
     // get root
-    number=arrays.find_number(number);
+    const auto number = arrays.find_number(*opt_num);
 
     assert(number<index_map.size());
     index_mapt::const_iterator it=index_map.find(number);

src/util/numbering.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <vector>
 
 #include <util/invariant.h>
+#include <util/optional.h>
 
 template <typename T>
 // NOLINTNEXTLINE(readability/identifiers)
@@ -60,15 +61,14 @@ class numbering final
     return number(a);
   }
 
-  bool get_number(const T &a, number_type &n) const
+  optionalt<number_type> get_number(const T &a) const
   {
-    typename numberst::const_iterator it=numbers.find(a);
-
-    if(it==numbers.end())
-      return true;
-
-    n=it->second;
-    return false;
+    const auto it = numbers.find(a);
+    if(it == numbers.end())
+    {
+      return {};
+    }
+    return it->second;
   }
 
   void clear()
@@ -129,15 +129,15 @@ class hash_numbering final
     return (result.first)->second;
   }
 
-  bool get_number(const T &a, number_type &n) const
+  optionalt<number_type> get_number(const T &a) const
   {
-    typename numberst::const_iterator it=numbers.find(a);
+    const auto it = numbers.find(a);
 
-    if(it==numbers.end())
-      return true;
-
-    n=it->second;
-    return false;
+    if(it == numbers.end())
+    {
+      return {};
+    }
+    return it->second;
   }
 
   void clear()

src/util/union_find.h

@@ -168,16 +168,14 @@ class union_find final
   // are 'a' and 'b' in the same set?
   bool same_set(const T &a, const T &b) const
   {
-    number_type na, nb;
-    bool have_na=!numbers.get_number(a, na),
-         have_nb=!numbers.get_number(b, nb);
+    const optionalt<number_type> na = numbers.get_number(a);
+    const optionalt<number_type> nb = numbers.get_number(a);
 
-    if(have_na && have_nb)
-      return uuf.same_set(na, nb);
-    else if(!have_na && !have_nb)
+    if(na && nb)
+      return uuf.same_set(*na, *nb);
+    if(!na && !nb)
       return a==b;
-    else
-      return false;
+    return false;
   }
 
   // are 'a' and 'b' in the same set?
@@ -259,9 +257,9 @@ class union_find final
     uuf.isolate(number(a));
   }
 
-  bool get_number(const T &a, number_type &n) const
+  optionalt<number_type> get_number(const T &a) const
   {
-    return numbers.get_number(a, n);
+    return numbers.get_number(a);
   }
 
   size_t size() const { return numbers.size(); }