avy: fixes to work with clang and musl

3 files changed, 149 insertions, 1 deletions

diff --git a/pkgs/applications/science/logic/avy/default.nix b/pkgs/applications/science/logic/avy/default.nix
index 379224c73f8..218006e15d5 100644
--- a/pkgs/applications/science/logic/avy/default.nix
+++ b/pkgs/applications/science/logic/avy/default.nix
@@ -12,7 +12,25 @@ stdenv.mkDerivation rec {
   };
 
   buildInputs = [ cmake zlib boost.out boost.dev ];
-  NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ];
+  NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ]
+    # Squelch endless stream of warnings on same few things
+    ++ stdenv.lib.optionals stdenv.cc.isClang [
+      "-Wno-empty-body"
+      "-Wno-tautological-compare"
+      "-Wc++11-compat-deprecated-writable-strings"
+      "-Wno-deprecated"
+    ];
+
+  prePatch = ''
+    sed -i -e '1i#include <stdint.h>' abc/src/bdd/dsd/dsd.h
+    substituteInPlace abc/src/bdd/dsd/dsd.h --replace \
+               '((Child = Dsd_NodeReadDec(Node,Index))>=0);' \
+               '((intptr_t)(Child = Dsd_NodeReadDec(Node,Index))>=0);'
+
+    patch -p1 -d minisat -i ${./minisat-fenv.patch}
+    patch -p1 -d glucose -i ${./glucose-fenv.patch}
+  '';
+
   patches =
     [ ./0001-no-static-boost-libs.patch
     ];
diff --git a/pkgs/applications/science/logic/avy/glucose-fenv.patch b/pkgs/applications/science/logic/avy/glucose-fenv.patch
new file mode 100644
index 00000000000..dd19f7ec80e
--- /dev/null
+++ b/pkgs/applications/science/logic/avy/glucose-fenv.patch
@@ -0,0 +1,65 @@
+From d6e0cb60270e8653bda3f339e3a07ce2cd2d6eb0 Mon Sep 17 00:00:00 2001
+From: Will Dietz <w@wdtz.org>
+Date: Tue, 17 Oct 2017 23:01:36 -0500
+Subject: [PATCH] glucose: use fenv to set double precision
+
+---
+ core/Main.cc   | 8 ++++++--
+ simp/Main.cc   | 8 ++++++--
+ utils/System.h | 2 +-
+ 3 files changed, 13 insertions(+), 5 deletions(-)
+
+diff --git a/core/Main.cc b/core/Main.cc
+index c96aadd..994132b 100644
+--- a/core/Main.cc
++++ b/core/Main.cc
+@@ -96,8 +96,12 @@ int main(int argc, char** argv)
+         // printf("This is MiniSat 2.0 beta\n");
+         
+ #if defined(__linux__)
+-        fpu_control_t oldcw, newcw;
+-        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
++        fenv_t fenv;
++
++        fegetenv(&fenv);
++        fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */
++        fenv.__control_word |= 0x200; /* _FPU_DOUBLE */
++        fesetenv(&fenv);
+         printf("c WARNING: for repeatability, setting FPU to use double precision\n");
+ #endif
+         // Extra options:
+diff --git a/simp/Main.cc b/simp/Main.cc
+index 4f4772d..70c2e4b 100644
+--- a/simp/Main.cc
++++ b/simp/Main.cc
+@@ -97,8 +97,12 @@ int main(int argc, char** argv)
+         
+         
+ #if defined(__linux__)
+-        fpu_control_t oldcw, newcw;
+-        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
++        fenv_t fenv;
++
++        fegetenv(&fenv);
++        fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */
++        fenv.__control_word |= 0x200; /* _FPU_DOUBLE */
++        fesetenv(&fenv);
+         printf("WARNING: for repeatability, setting FPU to use double precision\n");
+ #endif
+         // Extra options:
+diff --git a/utils/System.h b/utils/System.h
+index 004d498..a768e99 100644
+--- a/utils/System.h
++++ b/utils/System.h
+@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #define Glucose_System_h
+ 
+ #if defined(__linux__)
+-#include <fpu_control.h>
++#include <fenv.h>
+ #endif
+ 
+ #include "glucose/mtl/IntTypes.h"
+-- 
+2.14.2
+
diff --git a/pkgs/applications/science/logic/avy/minisat-fenv.patch b/pkgs/applications/science/logic/avy/minisat-fenv.patch
new file mode 100644
index 00000000000..686d5a1c5b4
--- /dev/null
+++ b/pkgs/applications/science/logic/avy/minisat-fenv.patch
@@ -0,0 +1,65 @@
+From 7f1016ceab9b0f57a935bd51ca6df3d18439b472 Mon Sep 17 00:00:00 2001
+From: Will Dietz <w@wdtz.org>
+Date: Tue, 17 Oct 2017 22:57:02 -0500
+Subject: [PATCH] use fenv instead of non-standard fpu_control
+
+---
+ core/Main.cc   | 8 ++++++--
+ simp/Main.cc   | 8 ++++++--
+ utils/System.h | 2 +-
+ 3 files changed, 13 insertions(+), 5 deletions(-)
+
+diff --git a/core/Main.cc b/core/Main.cc
+index 2b0d97b..8ad95fb 100644
+--- a/core/Main.cc
++++ b/core/Main.cc
+@@ -78,8 +78,12 @@ int main(int argc, char** argv)
+         // printf("This is MiniSat 2.0 beta\n");
+         
+ #if defined(__linux__)
+-        fpu_control_t oldcw, newcw;
+-        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
++        fenv_t fenv;
++
++        fegetenv(&fenv);
++        fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */
++        fenv.__control_word |= 0x200; /* _FPU_DOUBLE */
++        fesetenv(&fenv);
+         printf("WARNING: for repeatability, setting FPU to use double precision\n");
+ #endif
+         // Extra options:
+diff --git a/simp/Main.cc b/simp/Main.cc
+index 2804d7f..39bfb71 100644
+--- a/simp/Main.cc
++++ b/simp/Main.cc
+@@ -79,8 +79,12 @@ int main(int argc, char** argv)
+         // printf("This is MiniSat 2.0 beta\n");
+         
+ #if defined(__linux__)
+-        fpu_control_t oldcw, newcw;
+-        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
++        fenv_t fenv;
++
++        fegetenv(&fenv);
++        fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */
++        fenv.__control_word |= 0x200; /* _FPU_DOUBLE */
++        fesetenv(&fenv);
+         printf("WARNING: for repeatability, setting FPU to use double precision\n");
+ #endif
+         // Extra options:
+diff --git a/utils/System.h b/utils/System.h
+index 1758192..c0ad13a 100644
+--- a/utils/System.h
++++ b/utils/System.h
+@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #define Minisat_System_h
+ 
+ #if defined(__linux__)
+-#include <fpu_control.h>
++#include <fenv.h>
+ #endif
+ 
+ #include "mtl/IntTypes.h"
+-- 
+2.14.2
+