Ticket #31312: fix-clause-creator.diff

packages/swi-minisat2/C/SolverTypes.h

@@ -97 +97 @@
 //=================================================================================================
 // Clause -- a simple class for representing a clause:
 
-
 class Clause {
     uint32_t size_etc;
     union { float act; uint32_t abst; } extra;
@@ -116 +115 @@
         size_etc = (ps.size() << 3) | (uint32_t)learnt;
         for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
         if (learnt) extra.act = 0; else calcAbstraction(); }
-
     // -- use this function instead:
-    template<class V>
-    friend 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()));
-        return new (mem) Clause(ps, learnt); }
 
     int          size        ()      const   { return size_etc >> 3; }
     void         shrink      (int i)         { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
@@ -146 +138 @@
     void         strengthen  (Lit p);
 };
 
+template<class V>
+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()));
+    return new (mem) Clause(ps, learnt);
+}
+
 
 /*_________________________________________________________________________________________________
 |