Merge pull request #3871 from tautschnig/symbol_exprt-constant-propagator

Add an identifier-based lookup to constant_propagator_is_constantt [blocks: #3768]

Author: tautschnig

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

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