Move solver_factoryt definitions into .cpp file

Author: peterschrammel

src/goto-checker/solver_factory.cpp

@@ -28,6 +28,78 @@ Author: Daniel Kroening, Peter Schrammel
 #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.
 smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const

src/goto-checker/solver_factory.h

@@ -32,89 +32,35 @@ class 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;