Divide value-set of values from value-set of pointers

Stripped back value_set_abstract_object now it doesn't
have to deal with pointers.

Pulled out abstract_object_sett as a type not just an
alias. Add behaviour with functions pulled across from
value_set_abstract_objectt and
value_set_pointer_abstract_objectt.

Author: jezhiggins

src/analyses/Makefile

@@ -35,6 +35,7 @@ SRC = ai.cpp \
       uninitialized_domain.cpp \
       variable-sensitivity/abstract_environment.cpp \
       variable-sensitivity/abstract_object.cpp \
+      variable-sensitivity/abstract_object_set.cpp \
       variable-sensitivity/abstract_pointer_object.cpp \
       variable-sensitivity/abstract_value_object.cpp \
       variable-sensitivity/constant_abstract_value.cpp \
@@ -47,6 +48,7 @@ SRC = ai.cpp \
       variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \
       variable-sensitivity/value_set_abstract_value.cpp \
+      variable-sensitivity/value_set_pointer_abstract_object.cpp \
       variable-sensitivity/variable_sensitivity_configuration.cpp \
       variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
       variable-sensitivity/variable_sensitivity_domain.cpp \

src/analyses/variable-sensitivity/abstract_object_set.cpp

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/abstract_object_set.h>
+#include <util/string_utils.h>
+
+static bool by_length(const std::string &lhs, const std::string &rhs)
+{
+  if(lhs.size() < rhs.size())
+    return true;
+  if(lhs.size() > rhs.size())
+    return false;
+  return lhs < rhs;
+}
+
+void abstract_object_sett::output(
+  std::ostream &out,
+  const ai_baset &ai,
+  const namespacet &ns) const
+{
+  std::vector<std::string> output_values;
+  for(const auto &value : values)
+  {
+    std::ostringstream ss;
+    value->output(ss, ai, ns);
+    output_values.emplace_back(ss.str());
+  }
+  std::sort(output_values.begin(), output_values.end(), by_length);
+
+  join_strings(out, output_values.begin(), output_values.end(), ", ");
+}

src/analyses/variable-sensitivity/abstract_object_set.h

@@ -0,0 +1,83 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// an unordered set of value objects
+
+#ifndef CBMC_ABSTRACT_OBJECT_SET_H
+#define CBMC_ABSTRACT_OBJECT_SET_H
+
+#include <analyses/variable-sensitivity/abstract_value_object.h>
+#include <unordered_set>
+
+class abstract_object_sett
+{
+public:
+  using value_sett = std::unordered_set<
+    abstract_object_pointert,
+    abstract_hashert,
+    abstract_equalert>;
+  using const_iterator = value_sett::const_iterator;
+  using value_type = value_sett::value_type;
+  using size_type = value_sett::size_type;
+
+  void insert(const abstract_object_pointert &o)
+  {
+    values.insert(o);
+  }
+  void insert(abstract_object_pointert &&o)
+  {
+    values.insert(std::move(o));
+  }
+  void insert(const abstract_object_sett &rhs)
+  {
+    values.insert(rhs.begin(), rhs.end());
+  }
+
+  abstract_object_pointert first() const
+  {
+    return *begin();
+  }
+
+  const_iterator begin() const
+  {
+    return values.begin();
+  }
+  const_iterator end() const
+  {
+    return values.end();
+  }
+
+  value_sett::size_type size() const
+  {
+    return values.size();
+  }
+  bool empty() const
+  {
+    return values.empty();
+  }
+
+  bool operator==(const abstract_object_sett &rhs) const
+  {
+    return values == rhs.values;
+  }
+
+  void
+  output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
+
+private:
+  value_sett values;
+};
+
+class value_set_tag
+{
+public:
+  virtual const abstract_object_sett &get_values() const = 0;
+};
+
+#endif //CBMC_ABSTRACT_OBJECT_SET_H