Merge pull request #1590 from reuk/reuk/numbering-api-update

Don't mutate parameters in numbering class, remove duplication in numbering classes

Author: smowton

src/analyses/custom_bitvector_analysis.cpp

@@ -181,10 +181,10 @@ unsigned custom_bitvector_analysist::get_bit_nr(
   else if(string_expr.id()==ID_string_constant)
   {
     irep_idt value=string_expr.get(ID_value);
-    return bits(value);
+    return bits.number(value);
   }
   else
-    return bits("(unknown)");
+    return bits.number("(unknown)");
 }
 
 std::set<exprt> custom_bitvector_analysist::aliases(

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_constant.cpp

@@ -48,7 +48,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
   else if(expr_type.id()==ID_string)
   {
     // we use the numbering for strings
-    std::size_t number=string_numbering(expr.get_value());
+    std::size_t number = string_numbering.number(expr.get_value());
     return bv_utils.build_constant(number, bv.size());
   }
   else if(expr_type.id()==ID_range)

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

@@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #ifndef CPROVER_UTIL_NUMBERING_H
 #define CPROVER_UTIL_NUMBERING_H
 
@@ -16,154 +15,101 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <vector>
 
 #include <util/invariant.h>
+#include <util/optional.h>
 
-template <typename T>
-// NOLINTNEXTLINE(readability/identifiers)
-class numbering final
+/// \tparam Map a map from a key type to some numeric type
+template <typename Map>
+class template_numberingt final
 {
 public:
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef std::size_t number_type;
+  using number_type = typename Map::mapped_type; // NOLINT
+  using key_type = typename Map::key_type;       // NOLINT
 
 private:
-  typedef std::vector<T> data_typet;
-  data_typet data;
-  typedef std::map<T, number_type> numberst;
-  numberst numbers;
+  using data_typet = std::vector<key_type>; // NOLINT
+  data_typet data_;
+  Map numbers_;
 
 public:
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename data_typet::size_type size_type;
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename data_typet::iterator iterator;
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename data_typet::const_iterator const_iterator;
-
-  number_type number(const T &a)
+  using size_type = typename data_typet::size_type;           // NOLINT
+  using iterator = typename data_typet::iterator;             // NOLINT
+  using const_iterator = typename data_typet::const_iterator; // NOLINT
+
+  number_type number(const key_type &a)
   {
-    std::pair<typename numberst::const_iterator, bool> result=
-      numbers.insert(
-      std::pair<T, number_type>
-      (a, number_type(numbers.size())));
+    const auto result = numbers_.emplace(a, number_type(numbers_.size()));
 
     if(result.second) // inserted?
     {
-      data.push_back(a);
-      INVARIANT(data.size()==numbers.size(), "vector sizes must match");
+      data_.emplace_back(a);
+      INVARIANT(data_.size() == numbers_.size(), "vector sizes must match");
     }
 
     return (result.first)->second;
   }
 
-  number_type operator()(const T &a)
+  optionalt<number_type> get_number(const key_type &a) const
   {
-    return number(a);
+    const auto it = numbers_.find(a);
+    if(it == numbers_.end())
+    {
+      return {};
+    }
+    return it->second;
   }
 
-  bool get_number(const T &a, number_type &n) const
+  void clear()
   {
-    typename numberst::const_iterator it=numbers.find(a);
-
-    if(it==numbers.end())
-      return true;
-
-    n=it->second;
-    return false;
+    data_.clear();
+    numbers_.clear();
   }
 
-  void clear()
+  size_type size() const
   {
-    data.clear();
-    numbers.clear();
+    return data_.size();
   }
 
-  size_t size() const { return data.size(); }
-
-  T &operator[](size_type t) { return data[t]; }
-  const T &operator[](size_type t) const { return data[t]; }
-
-  iterator begin() { return data.begin(); }
-  const_iterator begin() const { return data.begin(); }
-  const_iterator cbegin() const { return data.cbegin(); }
-
-  iterator end() { return data.end(); }
-  const_iterator end() const { return data.end(); }
-  const_iterator cend() const { return data.cend(); }
-};
-
-template <typename T, class hash_fkt>
-// NOLINTNEXTLINE(readability/identifiers)
-class hash_numbering final
-{
-public:
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef unsigned int number_type;
-
-private:
-  typedef std::vector<T> data_typet;
-  data_typet data;
-  typedef std::unordered_map<T, number_type, hash_fkt> numberst;
-  numberst numbers;
-
-public:
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename data_typet::size_type size_type;
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename data_typet::iterator iterator;
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename data_typet::const_iterator const_iterator;
-
-  number_type number(const T &a)
+  key_type &operator[](size_type t)
   {
-    std::pair<typename numberst::const_iterator, bool> result=
-      numbers.insert(
-      std::pair<T, number_type>
-      (a, number_type(numbers.size())));
-
-    if(result.second) // inserted?
-    {
-      this->push_back(a);
-      assert(this->size()==numbers.size());
-    }
-
-    return (result.first)->second;
+    return data_[t];
   }
-
-  bool get_number(const T &a, number_type &n) const
+  const key_type &operator[](size_type t) const
   {
-    typename numberst::const_iterator it=numbers.find(a);
-
-    if(it==numbers.end())
-      return true;
-
-    n=it->second;
-    return false;
+    return data_[t];
   }
 
-  void clear()
+  iterator begin()
   {
-    data.clear();
-    numbers.clear();
+    return data_.begin();
+  }
+  const_iterator begin() const
+  {
+    return data_.begin();
+  }
+  const_iterator cbegin() const
+  {
+    return data_.cbegin();
   }
 
-  template <typename U>
-  void push_back(U &&u) { data.push_back(std::forward<U>(u)); }
-
-  T &operator[](size_type t) { return data[t]; }
-  const T &operator[](size_type t) const { return data[t]; }
-
-  T &at(size_type t) { return data.at(t); }
-  const T &at(size_type t) const { return data.at(t); }
-
-  size_type size() const { return data.size(); }
+  iterator end()
+  {
+    return data_.end();
+  }
+  const_iterator end() const
+  {
+    return data_.end();
+  }
+  const_iterator cend() const
+  {
+    return data_.cend();
+  }
+};
 
-  iterator begin() { return data.begin(); }
-  const_iterator begin() const { return data.begin(); }
-  const_iterator cbegin() const { return data.cbegin(); }
+template <typename Key>
+using numbering = template_numberingt<std::map<Key, std::size_t>>; // NOLINT
 
-  iterator end() { return data.end(); }
-  const_iterator end() const { return data.end(); }
-  const_iterator cend() const { return data.cend(); }
-};
+template <typename Key, typename Hash>
+using hash_numbering = // NOLINT
+  template_numberingt<std::unordered_map<Key, std::size_t, Hash>>;
 
 #endif // CPROVER_UTIL_NUMBERING_H

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(); }