Manage lifetime of MiniSat solver pointer using unique_ptr

This has the benefit of allowing the use of a default destructor rather
than a hand written destructor. Note that `satcheck_minisat2_baset` was
already non-copyable because its `solver_hardness` field was
non-copyable.

The default implementation of the destructor is in the `.cpp` rather
than the header file in order to avoid recompiling it every time the
header file is included.

Author: thomasspriggs

scripts/expected_doxygen_warnings.txt

@@ -6,14 +6,6 @@
   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_minisat2.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #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
@@ -309,21 +310,14 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
 template <typename T>
 satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
   message_handlert &message_handler)
-  : cnf_solvert(message_handler), solver(new T), 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

src/solvers/sat/satcheck_minisat2.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #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
@@ -30,6 +32,8 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
 {
 public:
   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();