Move goto_symex_is_constantt into its own file

No behavioural change.

Author: smowton

src/goto-symex/goto_symex_is_constant.h

@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: Symbolic Execution Constant Propagation
+
+Author: Michael Tautschig, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// GOTO Symex constant propagation
+
+#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
+#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
+
+#include <util/expr.h>
+#include <util/expr_util.h>
+
+class goto_symex_is_constantt : public is_constantt
+{
+protected:
+  bool is_constant(const exprt &expr) const override
+  {
+    if(expr.id() == ID_mult)
+    {
+      // propagate stuff with sizeof in it
+      forall_operands(it, expr)
+      {
+        if(it->find(ID_C_c_sizeof_type).is_not_nil())
+          return true;
+        else if(!is_constant(*it))
+          return false;
+      }
+
+      return true;
+    }
+    else if(expr.id() == ID_with)
+    {
+      // this is bad
+      /*
+      forall_operands(it, expr)
+      if(!is_constant(expr.op0()))
+      return false;
+
+      return true;
+      */
+      return false;
+    }
+
+    return is_constantt::is_constant(expr);
+  }
+};
+
+#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H

src/goto-symex/goto_symex_state.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 /// Symbolic Execution
 
 #include "goto_symex_state.h"
+#include "goto_symex_is_constant.h"
 
 #include <cstdlib>
 #include <iostream>
@@ -130,41 +131,6 @@ static bool check_renaming(const exprt &expr)
   return false;
 }
 
-class goto_symex_is_constantt : public is_constantt
-{
-protected:
-  bool is_constant(const exprt &expr) const override
-  {
-    if(expr.id() == ID_mult)
-    {
-      // propagate stuff with sizeof in it
-      forall_operands(it, expr)
-      {
-        if(it->find(ID_C_c_sizeof_type).is_not_nil())
-          return true;
-        else if(!is_constant(*it))
-          return false;
-      }
-
-      return true;
-    }
-    else if(expr.id() == ID_with)
-    {
-      // this is bad
-      /*
-      forall_operands(it, expr)
-      if(!is_constant(expr.op0()))
-      return false;
-
-      return true;
-      */
-      return false;
-    }
-
-    return is_constantt::is_constant(expr);
-  }
-};
-
 template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)