Make Glucose support compile

Hardness support was added to minisat2 only.

Author: tautschnig

src/solvers/sat/satcheck_glucose.cpp

@@ -121,6 +121,9 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
+    with_solver_hardness(
+      [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+
     clause_counter++;
   }
   catch(Glucose::OutOfMemoryException)

src/solvers/sat/satcheck_glucose.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "cnf.h"
 
+#include <solvers/hardness_collector.h>
+
 // Select one: basic solver or with simplification.
 // Note that the solver with simplifier isn't really robust
 // when used incrementally, as variables may disappear
@@ -23,8 +25,8 @@ class Solver; // NOLINT(readability/identifiers)
 class SimpSolver; // NOLINT(readability/identifiers)
 }
 
-template<typename T>
-class satcheck_glucose_baset:public cnf_solvert
+template <typename T>
+class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
 {
 public:
   satcheck_glucose_baset(T *, message_handlert &message_handler);
@@ -51,13 +53,29 @@ class satcheck_glucose_baset:public cnf_solvert
     return true;
   }
 
+  void
+  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
+  {
+    if(solver_hardness.has_value())
+    {
+      handler(solver_hardness.value());
+    }
+  }
+
+  void enable_hardness_collection() override
+  {
+    solver_hardness = solver_hardnesst{};
+  }
+
 protected:
   resultt do_prop_solve() override;
 
   T *solver;
 
   void add_variables();
   bvt assumptions;
+
+  optionalt<solver_hardnesst> solver_hardness;
 };
 
 class satcheck_glucose_no_simplifiert: