clang: allow to compile

Author: conp-solutions

coprocessor-src/BoundedVariableEliminationParallel.cc

@@ -960,9 +960,9 @@ void BoundedVariableElimination::parallelBVE(CoprocessorData& data)
     lastTouched.resize(data.nVars());
     VarOrderBVEHeapLt comp(data, config.opt_bve_heap);
     Heap<VarOrderBVEHeapLt> newheap(comp);
-    #ifdef __APPLE__
+    #if defined(__APPLE__) || defined(__clang__)
     BVEWorkData *workData = new BVEWorkData[ controller.size() ];
-    MethodFree mf(workData);
+    MethodArrayFree<BVEWorkData> mf(workData);
     #else
     BVEWorkData workData[ controller.size() ];
     #endif
@@ -1022,14 +1022,7 @@ void BoundedVariableElimination::parallelBVE(CoprocessorData& data)
             }
             if (config.opt_bve_verbose > 0) { cerr << "c parallel bve with " << controller.size() << " threads on " << QSize << " variables" << endl; }
             pthread_rwlock_t mutex = allocatorRWLock.getValue(); // FIXME reicht hier auch eine reference?
-            #ifndef __APPLE__ // Does not work on OS-X
-            assert(mutex.__data.__nr_readers == 0);
-            assert(mutex.__data.__readers_wakeup == 0);
-            assert(mutex.__data.__writer_wakeup == 0);
-            assert(mutex.__data.__nr_readers_queued == 0);
-            assert(mutex.__data.__writer == 0);
-            assert(mutex.__data.__lock == 0);
-            #endif
+
             controller.runJobs(jobs);
 
             if (!data.ok()) {

core/SolverTypes.h

@@ -68,7 +68,7 @@ struct Lit {
     int     x;
 
     // Use this as a constructor:
-    friend Lit mkLit(Var var, bool sign = false);
+    friend Lit mkLit(Var var, bool sign);
 
     bool operator == (Lit p) const { return x == p.x; }
     bool operator != (Lit p) const { return x != p.x; }
@@ -78,7 +78,7 @@ struct Lit {
 };
 
 
-inline  Lit  mkLit(Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline  Lit  mkLit(Var var, bool sign=false) { Lit p; p.x = var + var + (int)sign; return p; }
 inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
 inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
 inline  bool sign(Lit p)              { return p.x & 1; }
@@ -474,7 +474,7 @@ class Clause
     bool isShared() {      return header.shared == 0 ? false : true;    }
     //setting the shared to true... means the clause is shared or coming from a shared pool
     void setShared() {        header.shared = 1;    }
-    void initShCleanDelay(unsigned i) {        i > 1 ? header.shCleanDelay = 1 : header.shCleanDelay = i;    }
+    void initShCleanDelay(unsigned i) {header.shCleanDelay = i > 1 ? 1 : i;    }
     void decShCleanDelay() {        if (header.shCleanDelay > 0)     header.shCleanDelay--;    }
     unsigned getShCleanDelay() {       return header.shCleanDelay;    }
     #endif