Manage lifetime of Glucose 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_glucose_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 and so that the declaration of the solver
destructor is available when instantiating the destructor template of
`unique_ptr`.

Author: thomasspriggs

scripts/expected_doxygen_warnings.txt

@@ -1,11 +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()
-
 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, [email protected]
 #include <stack>
 
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/threeval.h>
 
 #include <core/Solver.h>
@@ -244,21 +245,12 @@ void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
 template <typename T>
 satcheck_glucose_baset<T>::satcheck_glucose_baset(
   message_handlert &message_handler)
-  : cnf_solvert(message_handler), solver(new T)
+  : 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

src/solvers/sat/satcheck_glucose.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_glucose_baset : public cnf_solvert, public hardness_collectort
 {
 public:
   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;