Merge pull request #5742 from tautschnig/simplify-cleanup-1

Make simplify_exprt::get_values file-local

Author: tautschnig

.clang-format

@@ -54,7 +54,6 @@ ForEachMacros: [
   'Forall_irep',
   'forall_named_irep',
   'Forall_named_irep',
-  'forall_value_list',
   'forall_symbol_base_map',
   'forall_subtypes',
   'Forall_subtypes']

regression/cbmc/inequality-with-constant-normalisation1/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
+int main()
+{
+  _Bool b1, b2;
+
+  int nc = (b1 ? 1 : 2) == (b2 ? 1 : 2);
+  assert(b1 != b2 || nc != 0);
+
+  // The following are true for all values of b1, b2, and the simplifier should
+  // be able to figure this out.
+  _Static_assert((b1 ? 1 : 1) == (b2 ? 1 : 1), "");
+  _Static_assert(((b1 ? 2 : 3) >= (b2 ? 1 : 2)) != 0, "");
+  _Static_assert(((b1 ? 0 : 1) >= (b2 ? 2 : 3)) == 0, "");
+  _Static_assert(((b1 ? 0 : 1) >= 2) == 0, "");
+}

regression/cbmc/inequality-with-constant-normalisation1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/util/simplify_expr.cpp

@@ -1331,31 +1331,6 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
   return unchanged(expr);
 }
 
-bool simplify_exprt::get_values(
-  const exprt &expr,
-  value_listt &value_list)
-{
-  if(expr.is_constant())
-  {
-    mp_integer int_value;
-    if(to_integer(to_constant_expr(expr), int_value))
-      return true;
-
-    value_list.insert(int_value);
-
-    return false;
-  }
-  else if(expr.id()==ID_if)
-  {
-    const auto &if_expr = to_if_expr(expr);
-
-    return get_values(if_expr.true_case(), value_list) ||
-           get_values(if_expr.false_case(), value_list);
-  }
-
-  return true;
-}
-
 simplify_exprt::resultt<>
 simplify_exprt::simplify_lambda(const lambda_exprt &expr)
 {

src/util/simplify_expr_class.h

@@ -66,10 +66,6 @@ class unary_plus_exprt;
 class update_exprt;
 class with_exprt;
 
-#define forall_value_list(it, value_list) \
-  for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \
-      it!=(value_list).end(); ++it)
-
 class simplify_exprt
 {
 public:
@@ -221,9 +217,6 @@ class simplify_exprt
 
   virtual bool simplify(exprt &expr);
 
-  typedef std::set<mp_integer> value_listt;
-  bool get_values(const exprt &expr, value_listt &value_list);
-
   static bool is_bitvector_type(const typet &type)
   {
     return type.id()==ID_unsignedbv ||

src/util/simplify_expr_int.cpp

@@ -1513,56 +1513,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
   if(expr.op0() == expr.op1())
     return true_exprt();
 
-  // try constants
-
-  value_listt values0, values1;
-
-  bool ok0=!get_values(expr.op0(), values0);
-  bool ok1=!get_values(expr.op1(), values1);
-
-  if(ok0 && ok1)
-  {
-    bool first=true;
-    bool result=false; // dummy initialization to prevent warning
-    bool ok=true;
-
-    // compare possible values
-
-    forall_value_list(it0, values0)
-      forall_value_list(it1, values1)
-      {
-        bool tmp;
-        const mp_integer &int_value0=*it0;
-        const mp_integer &int_value1=*it1;
-
-        if(expr.id()==ID_ge)
-          tmp=(int_value0>=int_value1);
-        else if(expr.id()==ID_equal)
-          tmp=(int_value0==int_value1);
-        else
-        {
-          tmp=false;
-          UNREACHABLE;
-        }
-
-        if(first)
-        {
-          result=tmp;
-          first=false;
-        }
-        else if(result!=tmp)
-        {
-          ok=false;
-          break;
-        }
-      }
-
-    if(ok)
-    {
-      return make_boolean_expr(result);
-    }
-  }
-
   // See if we can eliminate common addends on both sides.
   // On bit-vectors, this is only sound on '='.
   if(expr.id()==ID_equal)