minisat compile fix
authorClifford Wolf <clifford@clifford.at>
Sun, 20 Apr 2014 12:17:40 +0000 (14:17 +0200)
committerClifford Wolf <clifford@clifford.at>
Sun, 20 Apr 2014 12:17:40 +0000 (14:17 +0200)
libs/minisat/PATCH_mkLit_default_arg.patch [new file with mode: 0644]
libs/minisat/SolverTypes.h
libs/minisat/UPDATE.sh

diff --git a/libs/minisat/PATCH_mkLit_default_arg.patch b/libs/minisat/PATCH_mkLit_default_arg.patch
new file mode 100644 (file)
index 0000000..e21683f
--- /dev/null
@@ -0,0 +1,20 @@
+--- SolverTypes.h
++++ SolverTypes.h
+@@ -52,7 +52,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; }
+@@ -60,7 +60,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; }
index be40a4c372ac27020a50b548f59f72918a660db7..a47c2ce834ff554fb638af22ec6d499ecbc234ca 100644 (file)
@@ -52,7 +52,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; }
@@ -60,7 +60,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; }
index a84290279271b8a9ca18fa4cc83111753a77c9e4..68c7c60ee64eb23ec48b550c0df1f4159b2bd9fa 100644 (file)
@@ -11,3 +11,6 @@ sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc
 sed -i -e 's/PRI[iu]64/ & /' Options.h Solver.cc
 sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc
 sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc
+
+patch -p0 < PATCH_mkLit_default_arg.patch
+