Merge pull request #5548 from tautschnig/fix-glucose

Make Glucose support compile

Author: tautschnig

scripts/glucose-syrup-patch

@@ -98,6 +98,22 @@ diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
          throw OutOfMemoryException();
   }
 
+diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
+--- glucose-syrup/mtl/Vec.h
++++ glucose-syrup-patched/mtl/Vec.h
+@@ -103,8 +103,10 @@
+ void vec<T>::capacity(int min_cap) {
+     if (cap >= min_cap) return;
+     int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
+-    if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
+-        throw OutOfMemoryException();
++    if (add > INT_MAX - cap)
++      throw OutOfMemoryException();
++
++    data = (T*)xrealloc(data, (cap += add) * sizeof(T));
+  }
+ 
+ 
 diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
 --- glucose-syrup/simp/SimpSolver.cc	2014-10-03 11:10:22.000000000 +0200
 +++ glucose-syrup-patched/simp/SimpSolver.cc	2018-04-21 16:58:22.950005391 +0200
@@ -201,6 +217,15 @@ diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUt
 
      int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
      void operator ++ ()       { pos++; assureLookahead(); }
+@@ -96,7 +96,7 @@
+ 	if (*in != '.') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
+ 	++in; // skip dot
+ 	currentExponent = 0.1;
+-    while (*in >= '0' && *in <= '9')
++	while (*in >= '0' && *in <= '9')
+         accu = accu + currentExponent * ((double)(*in - '0')),
+ 		currentExponent /= 10,
+         ++in;
 diff -rupNw glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
 --- glucose-syrup/utils/System.h	2014-10-03 11:10:22.000000000 +0200
 +++ glucose-syrup-patched/utils/System.h	2018-04-21 16:58:22.950005391 +0200

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: