From 4455fb5ebed5e61deca4995f0f61e0a19061e646 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 21 Jan 2019 12:17:06 +0000
Subject: [PATCH] Add an identifier-based lookup to
 constant_propagator_is_constantt

This avoid the workaround of constructing a symbol_exprt without proper type
just for the sake of a lookup.
---
 src/analyses/constant_propagator.cpp | 53 +++++++++++++++-------------
 src/analyses/constant_propagator.h   |  2 ++
 2 files changed, 31 insertions(+), 24 deletions(-)

diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index b4368cfc5cd..781303d16ee 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -415,36 +415,42 @@ bool constant_propagator_domaint::ai_simplify(
   return partial_evaluate(values, condition, ns);
 }
 
-
-bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
+class constant_propagator_is_constantt : public is_constantt
 {
-  class constant_propagator_is_constantt : public is_constantt
+public:
+  explicit constant_propagator_is_constantt(
+    const replace_symbolt &replace_const)
+    : replace_const(replace_const)
   {
-  public:
-    explicit constant_propagator_is_constantt(
-      const replace_symbolt &replace_const)
-      : replace_const(replace_const)
-    {
-    }
+  }
 
-  protected:
-    bool is_constant(const exprt &expr) const override
-    {
-      if(expr.id() == ID_symbol)
-      {
-        return replace_const.replaces_symbol(
-          to_symbol_expr(expr).get_identifier());
-      }
+  bool is_constant(const irep_idt &id) const
+  {
+    return replace_const.replaces_symbol(id);
+  }
 
-      return is_constantt::is_constant(expr);
-    }
+protected:
+  bool is_constant(const exprt &expr) const override
+  {
+    if(expr.id() == ID_symbol)
+      return is_constant(to_symbol_expr(expr).get_identifier());
+
+    return is_constantt::is_constant(expr);
+  }
 
-    const replace_symbolt &replace_const;
-  };
+  const replace_symbolt &replace_const;
+};
 
+bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
+{
   return constant_propagator_is_constantt(replace_const)(expr);
 }
 
+bool constant_propagator_domaint::valuest::is_constant(const irep_idt &id) const
+{
+  return constant_propagator_is_constantt(replace_const).is_constant(id);
+}
+
 /// Do not call this when iterating over replace_const.expr_map!
 bool constant_propagator_domaint::valuest::set_to_top(
   const symbol_exprt &symbol_expr)
@@ -649,10 +655,9 @@ bool constant_propagator_domaint::partial_evaluate(
   // if the current rounding mode is top we can
   // still get a non-top result by trying all rounding
   // modes and checking if the results are all the same
-  if(!known_values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str)))
-  {
+  if(!known_values.is_constant(ID_cprover_rounding_mode_str))
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
-  }
+
   return replace_constants_and_simplify(known_values, expr, ns);
 }
 
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 2d995efb984..698970b4b30 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -125,6 +125,8 @@ class constant_propagator_domaint:public ai_domain_baset
 
     bool is_constant(const exprt &expr) const;
 
+    bool is_constant(const irep_idt &id) const;
+
     bool is_empty() const
     {
       return replace_const.empty();