Merge pull request #6078 from thomasspriggs/tas/solver_unique_ptr

Manage lifetime of MiniSat and Glucose solver pointers using unique_ptr

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -1,19 +1,3 @@
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:246: warning: no matching class member found for 
-  template
-  satcheck_glucose_baset< Glucose::Solver >::~satcheck_glucose_baset()
-
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:252: warning: no matching class member found for 
-  template
-  satcheck_glucose_baset< Glucose::SimpSolver >::~satcheck_glucose_baset()
-
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:313: warning: no matching class member found for 
-  template
-  satcheck_minisat2_baset< Minisat::Solver >::~satcheck_minisat2_baset()
-
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:319: warning: no matching class member found for 
-  template
-  satcheck_minisat2_baset< Minisat::SimpSolver >::~satcheck_minisat2_baset()
-
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/solvers/sat/satcheck_glucose.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <stack>
 
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/threeval.h>
 
 #include <core/Solver.h>
@@ -243,23 +244,13 @@ void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
 
 template <typename T>
 satcheck_glucose_baset<T>::satcheck_glucose_baset(
-  T *_solver,
   message_handlert &message_handler)
-  : cnf_solvert(message_handler), solver(_solver)
+  : cnf_solvert(message_handler), solver(util_make_unique<T>())
 {
 }
 
-template<>
-satcheck_glucose_baset<Glucose::Solver>::~satcheck_glucose_baset()
-{
-  delete solver;
-}
-
-template<>
-satcheck_glucose_baset<Glucose::SimpSolver>::~satcheck_glucose_baset()
-{
-  delete solver;
-}
+template <typename T>
+satcheck_glucose_baset<T>::~satcheck_glucose_baset() = default;
 
 template<typename T>
 bool satcheck_glucose_baset<T>::is_in_conflict(literalt a) const
@@ -285,21 +276,8 @@ void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
   }
 }
 
-satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(
-  message_handlert &message_handler)
-  : satcheck_glucose_baset<Glucose::Solver>(
-      new Glucose::Solver,
-      message_handler)
-{
-}
-
-satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
-  message_handlert &message_handler)
-  : satcheck_glucose_baset<Glucose::SimpSolver>(
-      new Glucose::SimpSolver,
-      message_handler)
-{
-}
+template class satcheck_glucose_baset<Glucose::Solver>;
+template class satcheck_glucose_baset<Glucose::SimpSolver>;
 
 void satcheck_glucose_simplifiert::set_frozen(literalt a)
 {

src/solvers/sat/satcheck_glucose.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/hardness_collector.h>
 
+#include <memory>
+
 // Select one: basic solver or with simplification.
 // Note that the solver with simplifier isn't really robust
 // when used incrementally, as variables may disappear
@@ -29,8 +31,10 @@ template <typename T>
 class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
 {
 public:
-  satcheck_glucose_baset(T *, message_handlert &message_handler);
-  virtual ~satcheck_glucose_baset();
+  explicit satcheck_glucose_baset(message_handlert &message_handler);
+  /// A default destructor defined in the `.cpp` is used to ensure the
+  /// unique_ptr to the solver is correctly destroyed.
+  ~satcheck_glucose_baset() override;
 
   tvt l_get(literalt a) const override;
 
@@ -70,7 +74,7 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
 protected:
   resultt do_prop_solve() override;
 
-  T *solver;
+  std::unique_ptr<T> solver;
 
   void add_variables();
   bvt assumptions;
@@ -82,15 +86,15 @@ class satcheck_glucose_no_simplifiert:
   public satcheck_glucose_baset<Glucose::Solver>
 {
 public:
-  explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
+  using satcheck_glucose_baset<Glucose::Solver>::satcheck_glucose_baset;
   const std::string solver_text() override;
 };
 
 class satcheck_glucose_simplifiert:
   public satcheck_glucose_baset<Glucose::SimpSolver>
 {
 public:
-  explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
+  using satcheck_glucose_baset<Glucose::SimpSolver>::satcheck_glucose_baset;
   const std::string solver_text() override;
   void set_frozen(literalt a) override;
   bool is_eliminated(literalt a) const;

src/solvers/sat/satcheck_minisat2.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <stack>
 
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/threeval.h>
 
 #include <minisat/core/Solver.h>
@@ -227,7 +228,7 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
 
     if(time_limit_seconds != 0)
     {
-      solver_to_interrupt = solver;
+      solver_to_interrupt = solver.get();
       old_handler = signal(SIGALRM, interrupt_solver);
       if(old_handler == SIG_ERR)
         log.warning() << "Failed to set solver time limit" << messaget::eom;
@@ -241,7 +242,7 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
     {
       alarm(0);
       signal(SIGALRM, old_handler);
-      solver_to_interrupt = solver;
+      solver_to_interrupt = solver.get();
     }
 
 #else // _WIN32
@@ -308,23 +309,15 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
 
 template <typename T>
 satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
-  T *_solver,
   message_handlert &message_handler)
-  : cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
+  : cnf_solvert(message_handler),
+    solver(util_make_unique<T>()),
+    time_limit_seconds(0)
 {
 }
 
-template<>
-satcheck_minisat2_baset<Minisat::Solver>::~satcheck_minisat2_baset()
-{
-  delete solver;
-}
-
-template<>
-satcheck_minisat2_baset<Minisat::SimpSolver>::~satcheck_minisat2_baset()
-{
-  delete solver;
-}
+template <typename T>
+satcheck_minisat2_baset<T>::~satcheck_minisat2_baset() = default;
 
 template<typename T>
 bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const
@@ -353,21 +346,8 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
   }
 }
 
-satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
-  message_handlert &message_handler)
-  : satcheck_minisat2_baset<Minisat::Solver>(
-      new Minisat::Solver,
-      message_handler)
-{
-}
-
-satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
-  message_handlert &message_handler)
-  : satcheck_minisat2_baset<Minisat::SimpSolver>(
-      new Minisat::SimpSolver,
-      message_handler)
-{
-}
+template class satcheck_minisat2_baset<Minisat::Solver>;
+template class satcheck_minisat2_baset<Minisat::SimpSolver>;
 
 void satcheck_minisat_simplifiert::set_frozen(literalt a)
 {

src/solvers/sat/satcheck_minisat2.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/hardness_collector.h>
 
+#include <memory>
+
 // Select one: basic solver or with simplification.
 // Note that the solver with simplifier isn't really robust
 // when used incrementally, as variables may disappear
@@ -29,8 +31,10 @@ template <typename T>
 class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
 {
 public:
-  satcheck_minisat2_baset(T *, message_handlert &message_handler);
-  virtual ~satcheck_minisat2_baset();
+  explicit satcheck_minisat2_baset(message_handlert &message_handler);
+  /// A default destructor defined in the `.cpp` is used to ensure the
+  /// unique_ptr to the solver is correctly destroyed.
+  ~satcheck_minisat2_baset() override;
 
   tvt l_get(literalt a) const override final;
 
@@ -81,7 +85,7 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
 protected:
   resultt do_prop_solve() override;
 
-  T *solver;
+  std::unique_ptr<T> solver;
   uint32_t time_limit_seconds;
 
   void add_variables();
@@ -94,15 +98,15 @@ class satcheck_minisat_no_simplifiert:
   public satcheck_minisat2_baset<Minisat::Solver>
 {
 public:
-  explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
+  using satcheck_minisat2_baset<Minisat::Solver>::satcheck_minisat2_baset;
   const std::string solver_text() override;
 };
 
 class satcheck_minisat_simplifiert:
   public satcheck_minisat2_baset<Minisat::SimpSolver>
 {
 public:
-  explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
+  using satcheck_minisat2_baset<Minisat::SimpSolver>::satcheck_minisat2_baset;
   const std::string solver_text() override final;
   void set_frozen(literalt a) override final;
   bool is_eliminated(literalt a) const;