Avoid Doxygen warnings for MiniSat and Glucose

Move the destructor to the non-template class.

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

@@ -249,18 +249,6 @@ satcheck_glucose_baset<T>::satcheck_glucose_baset(
 {
 }
 
-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>
 bool satcheck_glucose_baset<T>::is_in_conflict(literalt a) const
 {
@@ -293,6 +281,11 @@ satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(
 {
 }
 
+satcheck_glucose_no_simplifiert::~satcheck_glucose_no_simplifiert()
+{
+  delete solver;
+}
+
 satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
   message_handlert &message_handler)
   : satcheck_glucose_baset<Glucose::SimpSolver>(
@@ -301,6 +294,11 @@ satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
 {
 }
 
+satcheck_glucose_simplifiert::~satcheck_glucose_simplifiert()
+{
+  delete solver;
+}
+
 void satcheck_glucose_simplifiert::set_frozen(literalt a)
 {
   try

src/solvers/sat/satcheck_glucose.h

@@ -30,7 +30,6 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
 {
 public:
   satcheck_glucose_baset(T *, message_handlert &message_handler);
-  virtual ~satcheck_glucose_baset();
 
   tvt l_get(literalt a) const override;
 
@@ -68,6 +67,10 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
   }
 
 protected:
+  // This class needs to be inherited from, and inheriting classes need to
+  // delete `solver` in their destructor.
+  virtual ~satcheck_glucose_baset() = default;
+
   resultt do_prop_solve() override;
 
   T *solver;
@@ -83,6 +86,7 @@ class satcheck_glucose_no_simplifiert:
 {
 public:
   explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
+  ~satcheck_glucose_no_simplifiert() override;
   const std::string solver_text() override;
 };
 
@@ -91,6 +95,7 @@ class satcheck_glucose_simplifiert:
 {
 public:
   explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
+  ~satcheck_glucose_simplifiert() override;
   const std::string solver_text() override;
   void set_frozen(literalt a) override;
   bool is_eliminated(literalt a) const;

src/solvers/sat/satcheck_minisat2.cpp

@@ -312,18 +312,6 @@ satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
 {
 }
 
-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>
 bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const
 {
@@ -359,6 +347,11 @@ satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
 {
 }
 
+satcheck_minisat_no_simplifiert::~satcheck_minisat_no_simplifiert()
+{
+  delete solver;
+}
+
 satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
   message_handlert &message_handler)
   : satcheck_minisat2_baset<Minisat::SimpSolver>(
@@ -367,6 +360,11 @@ satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
 {
 }
 
+satcheck_minisat_simplifiert::~satcheck_minisat_simplifiert()
+{
+  delete solver;
+}
+
 void satcheck_minisat_simplifiert::set_frozen(literalt a)
 {
   try

src/solvers/sat/satcheck_minisat2.h

@@ -30,7 +30,6 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
 {
 public:
   satcheck_minisat2_baset(T *, message_handlert &message_handler);
-  virtual ~satcheck_minisat2_baset();
 
   tvt l_get(literalt a) const override final;
 
@@ -79,6 +78,10 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
   }
 
 protected:
+  // This class needs to be inherited from, and inheriting classes need to
+  // delete `solver` in their destructor.
+  virtual ~satcheck_minisat2_baset() = default;
+
   resultt do_prop_solve() override;
 
   T *solver;
@@ -95,6 +98,7 @@ class satcheck_minisat_no_simplifiert:
 {
 public:
   explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
+  ~satcheck_minisat_no_simplifiert() override;
   const std::string solver_text() override;
 };
 
@@ -103,6 +107,7 @@ class satcheck_minisat_simplifiert:
 {
 public:
   explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
+  ~satcheck_minisat_simplifiert() override;
   const std::string solver_text() override final;
   void set_frozen(literalt a) override final;
   bool is_eliminated(literalt a) const;