Merge pull request #4244 from tautschnig/include-cleanup

Remove unused includes list, functional from expr.h

Author: tautschnig

src/ansi-c/ansi_c_convert_type.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
 #define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
 
+#include <list>
+
 #include <util/message.h>
 
 #include "c_qualifiers.h"

src/assembler/assembler_parser.cpp

@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "assembler_parser.h"
 
-#include <iostream>
-
 assembler_parsert assembler_parser;
 
 extern char *yyassemblertext;

src/assembler/assembler_parser.h

@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H
 
 #include <util/parser.h>
-#include <util/expr.h>
+
+#include <list>
 
 int yyassemblerlex();
 int yyassemblererror(const std::string &error);

src/cbmc/all_properties.cpp

@@ -20,8 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/xml.h>
 #include <util/json.h>
 
+#include <solvers/prop/prop_conv.h>
 #include <solvers/sat/satcheck.h>
-#include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>

src/cbmc/all_properties_class.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
 
 #include <solvers/prop/cover_goals.h>
+#include <solvers/prop/literal_expr.h>
 
 #include "bmc.h"
 

src/cbmc/bmc_cover.cpp

@@ -21,7 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/xml_irep.h>
 
 #include <solvers/prop/cover_goals.h>
-#include <solvers/prop/literal_expr.h>
+#include <solvers/prop/prop_conv.h>
 
 #include <goto-symex/build_goto_trace.h>
 

src/solvers/flattening/arrays.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_FLATTENING_ARRAYS_H
 #define CPROVER_SOLVERS_FLATTENING_ARRAYS_H
 
+#include <list>
 #include <set>
 
 #include <util/union_find.h>

src/solvers/prop/cover_goals.cpp

@@ -11,9 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "cover_goals.h"
 
-#include <util/threeval.h>
-
 #include "literal_expr.h"
+#include "prop_conv.h"
 
 cover_goalst::~cover_goalst()
 {

src/solvers/prop/cover_goals.h

@@ -12,9 +12,14 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_PROP_COVER_GOALS_H
 #define CPROVER_SOLVERS_PROP_COVER_GOALS_H
 
+#include <list>
+
+#include <util/decision_procedure.h>
 #include <util/message.h>
 
-#include "prop_conv.h"
+#include "literal.h"
+
+class prop_convt;
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.

src/util/expr.h

@@ -15,9 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include "validate_types.h"
 #include "validation_mode.h"
 
-#include <functional>
-#include <list>
-
 #define forall_operands(it, expr) \
   if((expr).has_operands()) /* NOLINT(readability/braces) */ \
     for(exprt::operandst::const_iterator it=(expr).operands().begin(), \