Optimize imports

Author: peterschrammel

src/goto-checker/solver_factory.cpp

@@ -11,22 +11,23 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "solver_factory.h"
 
-#include <fstream>
 #include <iostream>
-#include <memory>
-#include <string>
 
 #include <util/exception_utils.h>
 #include <util/make_unique.h>
-#include <util/unicode.h>
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/options.h>
+#include <util/symbol_table.h>
 #include <util/version.h>
 
 #include <solvers/flattening/bv_dimacs.h>
+#include <solvers/prop/prop.h>
+#include <solvers/prop/prop_conv.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement.h>
 #include <solvers/sat/dimacs_cnf.h>
 #include <solvers/sat/satcheck.h>
-#include <solvers/smt2/smt2_dec.h>
 
 solver_factoryt::solver_factoryt(
   const optionst &_options,
@@ -41,10 +42,6 @@ solver_factoryt::solver_factoryt(
 {
 }
 
-solver_factoryt::solvert::solvert()
-{
-}
-
 solver_factoryt::solvert::solvert(std::unique_ptr<prop_convt> p)
   : prop_conv_ptr(std::move(p))
 {
@@ -104,10 +101,6 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
   return get_default();
 }
 
-solver_factoryt::~solver_factoryt()
-{
-}
-
 /// Uses the options to pick an SMT 2.0 solver
 /// \return An smt2_dect::solvert giving the solver to use.
 smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const

src/goto-checker/solver_factory.h

@@ -12,19 +12,17 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 #define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
 
-#include <list>
-#include <map>
 #include <memory>
 
-#include <util/options.h>
-
-#include <goto-symex/symex_target_equation.h>
-#include <solvers/prop/prop.h>
-#include <solvers/prop/prop_conv.h>
-#include <solvers/sat/cnf.h>
-#include <solvers/sat/satcheck.h>
 #include <solvers/smt2/smt2_dec.h>
 
+class message_handlert;
+class namespacet;
+class optionst;
+class propt;
+class prop_convt;
+class symbol_tablet;
+
 class solver_factoryt
 {
 public:
@@ -39,7 +37,7 @@ class solver_factoryt
   class solvert
   {
   public:
-    solvert();
+    solvert() = default;
     explicit solvert(std::unique_ptr<prop_convt> p);
     solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2);
     solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2);
@@ -60,7 +58,7 @@ class solver_factoryt
   /// Returns a solvert object
   virtual std::unique_ptr<solvert> get_solver();
 
-  virtual ~solver_factoryt();
+  virtual ~solver_factoryt() = default;
 
 protected:
   const optionst &options;