Merge pull request #3588 from peterschrammel/improve-solver-factory

Improve solver factory

Author: peterschrammel

src/goto-checker/solver_factory.cpp

@@ -11,22 +11,99 @@ 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>
 
+#ifdef _MSC_VER
+#include <util/unicode.h>
+#endif
+
 #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,
+  const symbol_tablet &_symbol_table,
+  message_handlert &_message_handler,
+  bool _output_xml_in_refinement)
+  : options(_options),
+    symbol_table(_symbol_table),
+    ns(_symbol_table),
+    message_handler(_message_handler),
+    output_xml_in_refinement(_output_xml_in_refinement)
+{
+}
+
+solver_factoryt::solvert::solvert(std::unique_ptr<prop_convt> p)
+  : prop_conv_ptr(std::move(p))
+{
+}
+
+solver_factoryt::solvert::solvert(
+  std::unique_ptr<prop_convt> p1,
+  std::unique_ptr<propt> p2)
+  : prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
+{
+}
+
+solver_factoryt::solvert::solvert(
+  std::unique_ptr<prop_convt> p1,
+  std::unique_ptr<std::ofstream> p2)
+  : ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
+{
+}
+
+prop_convt &solver_factoryt::solvert::prop_conv() const
+{
+  PRECONDITION(prop_conv_ptr != nullptr);
+  return *prop_conv_ptr;
+}
+
+propt &solver_factoryt::solvert::prop() const
+{
+  PRECONDITION(prop_ptr != nullptr);
+  return *prop_ptr;
+}
+
+void solver_factoryt::solvert::set_prop_conv(std::unique_ptr<prop_convt> p)
+{
+  prop_conv_ptr = std::move(p);
+}
+
+void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
+{
+  prop_ptr = std::move(p);
+}
+
+void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
+{
+  ofstream_ptr = std::move(p);
+}
+
+std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
+{
+  if(options.get_bool_option("dimacs"))
+    return get_dimacs();
+  if(options.get_bool_option("refine"))
+    return get_bv_refinement();
+  else if(options.get_bool_option("refine-strings"))
+    return get_string_refinement();
+  if(options.get_bool_option("smt2"))
+    return get_smt2(get_smt2_solver_type());
+  return get_default();
+}
 
 /// Uses the options to pick an SMT 2.0 solver
 /// \return An smt2_dect::solvert giving the solver to use.

src/goto-checker/solver_factory.h

@@ -12,109 +12,53 @@ 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:
   solver_factoryt(
     const optionst &_options,
     const symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _output_xml_in_refinement)
-    : options(_options),
-      symbol_table(_symbol_table),
-      ns(_symbol_table),
-      message_handler(_message_handler),
-      output_xml_in_refinement(_output_xml_in_refinement)
-  {
-  }
+    bool _output_xml_in_refinement);
 
   // The solver class,
   // which owns a variety of allocated objects.
   class solvert
   {
   public:
-    solvert()
-    {
-    }
-
-    explicit solvert(std::unique_ptr<prop_convt> p)
-      : prop_conv_ptr(std::move(p))
-    {
-    }
-
-    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2)
-      : prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
-    {
-    }
-
-    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2)
-      : ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
-    {
-    }
-
-    prop_convt &prop_conv() const
-    {
-      PRECONDITION(prop_conv_ptr != nullptr);
-      return *prop_conv_ptr;
-    }
-
-    propt &prop() const
-    {
-      PRECONDITION(prop_ptr != nullptr);
-      return *prop_ptr;
-    }
-
-    void set_prop_conv(std::unique_ptr<prop_convt> p)
-    {
-      prop_conv_ptr = std::move(p);
-    }
-
-    void set_prop(std::unique_ptr<propt> p)
-    {
-      prop_ptr = std::move(p);
-    }
-
-    void set_ofstream(std::unique_ptr<std::ofstream> p)
-    {
-      ofstream_ptr = std::move(p);
-    }
+    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);
+
+    prop_convt &prop_conv() const;
+    propt &prop() const;
+
+    void set_prop_conv(std::unique_ptr<prop_convt> p);
+    void set_prop(std::unique_ptr<propt> p);
+    void set_ofstream(std::unique_ptr<std::ofstream> p);
 
     // the objects are deleted in the opposite order they appear below
     std::unique_ptr<std::ofstream> ofstream_ptr;
     std::unique_ptr<propt> prop_ptr;
     std::unique_ptr<prop_convt> prop_conv_ptr;
   };
 
-  // returns a solvert object
-  virtual std::unique_ptr<solvert> get_solver()
-  {
-    if(options.get_bool_option("dimacs"))
-      return get_dimacs();
-    if(options.get_bool_option("refine"))
-      return get_bv_refinement();
-    else if(options.get_bool_option("refine-strings"))
-      return get_string_refinement();
-    if(options.get_bool_option("smt2"))
-      return get_smt2(get_smt2_solver_type());
-    return get_default();
-  }
-
-  virtual ~solver_factoryt()
-  {
-  }
+  /// Returns a solvert object
+  virtual std::unique_ptr<solvert> get_solver();
+
+  virtual ~solver_factoryt() = default;
 
 protected:
   const optionst &options;