From d71beac1a3d831da1a30663adca08c001222dd05 Mon Sep 17 00:00:00 2001
From: u-u-h <lisp@uuhaus.de>
Date: Tue, 31 May 2016 10:45:56 +0200
Subject: [PATCH] fix minisat compile on modern c++ compilers

---
 backends/minisat/core/Solver.C      |  4 ++--
 backends/minisat/core/SolverTypes.h |  2 +-
 backends/minisat/simp/SimpSolver.C  | 10 ++++++----
 backends/precosat/precosat.hh       |  1 +
 4 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/backends/minisat/core/Solver.C b/backends/minisat/core/Solver.C
index 404f4da..567a02c 100644
--- a/backends/minisat/core/Solver.C
+++ b/backends/minisat/core/Solver.C
@@ -114,7 +114,7 @@ bool Solver::addClause(vec<Lit>& ps)
         uncheckedEnqueue(ps[0]);
         return ok = (propagate() == NULL);
     }else{
-        Clause* c = Clause_new(ps, false);
+        Clause* c = Clause::Clause_new(ps, false);
         clauses.push(c);
         attachClause(*c);
     }
@@ -572,7 +572,7 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
             if (learnt_clause.size() == 1){
                 uncheckedEnqueue(learnt_clause[0]);
             }else{
-                Clause* c = Clause_new(learnt_clause, true);
+                Clause* c = Clause::Clause_new(learnt_clause, true);
                 learnts.push(c);
                 attachClause(*c);
                 claBumpActivity(*c);
diff --git a/backends/minisat/core/SolverTypes.h b/backends/minisat/core/SolverTypes.h
index 47e3023..919b60b 100644
--- a/backends/minisat/core/SolverTypes.h
+++ b/backends/minisat/core/SolverTypes.h
@@ -119,7 +119,7 @@ public:
 
     // -- use this function instead:
     template<class V>
-    friend Clause* Clause_new(const V& ps, bool learnt = false) {
+    static Clause* Clause_new(const V& ps, bool learnt = false) {
         assert(sizeof(Lit)      == sizeof(uint32_t));
         assert(sizeof(float)    == sizeof(uint32_t));
         void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
diff --git a/backends/minisat/simp/SimpSolver.C b/backends/minisat/simp/SimpSolver.C
index 22121c3..ea027b5 100644
--- a/backends/minisat/simp/SimpSolver.C
+++ b/backends/minisat/simp/SimpSolver.C
@@ -38,7 +38,7 @@ SimpSolver::SimpSolver() :
   , bwdsub_assigns     (0)
 {
     vec<Lit> dummy(1,lit_Undef);
-    bwdsub_tmpunit   = Clause_new(dummy);
+    bwdsub_tmpunit   = Clause::Clause_new(dummy);
     remove_satisfied = false;
 }
 
@@ -224,11 +224,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     for (int i = 0; i < qs.size(); i++){
         if (var(qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
-                if (var(ps[j]) == var(qs[i]))
+                if (var(ps[j]) == var(qs[i])) {
                     if (ps[j] == ~qs[i])
                         return false;
                     else
                         goto next;
+		}
             out_clause.push(qs[i]);
         }
         next:;
@@ -256,11 +257,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
     for (int i = 0; i < qs.size(); i++){
         if (var(__qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
-                if (var(__ps[j]) == var(__qs[i]))
+                if (var(__ps[j]) == var(__qs[i])) {
                     if (__ps[j] == ~__qs[i])
                         return false;
                     else
                         goto next;
+		}
         }
         next:;
     }
@@ -470,7 +472,7 @@ bool SimpSolver::eliminateVar(Var v, bool fail)
     elimtable[v].order = elimorder++;
     assert(elimtable[v].eliminated.size() == 0);
     for (int i = 0; i < cls.size(); i++){
-        elimtable[v].eliminated.push(Clause_new(*cls[i]));
+        elimtable[v].eliminated.push(Clause::Clause_new(*cls[i]));
         removeClause(*cls[i]); }
 
     // Produce clauses in cross product:
diff --git a/backends/precosat/precosat.hh b/backends/precosat/precosat.hh
index 0b95058..cff9847 100644
--- a/backends/precosat/precosat.hh
+++ b/backends/precosat/precosat.hh
@@ -29,6 +29,7 @@ IN THE SOFTWARE.
 #include <cstdarg>
 #include <cstring>
 #include <cstdio>
+#include <cstddef>
 
 namespace PrecoSat {
 
-- 
2.11.4.GIT