From 12e60c232a7691510dc8b13f069bd1c89e8eaaa7 Mon Sep 17 00:00:00 2001
From: Will Dietz <w@wdtz.org>
Date: Wed, 8 Nov 2017 12:20:50 -0600
Subject: cvc4: patch up fpu_control usage

---
 pkgs/applications/science/logic/cvc4/default.nix   |  5 ++
 .../science/logic/cvc4/minisat-fenv.patch          | 65 ++++++++++++++++++++++
 2 files changed, 70 insertions(+)
 create mode 100644 pkgs/applications/science/logic/cvc4/minisat-fenv.patch

(limited to 'pkgs/applications/science/logic/cvc4')

diff --git a/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix
index 6b213226635..25effdcd403 100644
--- a/pkgs/applications/science/logic/cvc4/default.nix
+++ b/pkgs/applications/science/logic/cvc4/default.nix
@@ -22,6 +22,11 @@ stdenv.mkDerivation rec {
     "--with-boost=${boost.dev}"
   ];
 
+  prePatch = ''
+    patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat
+    patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat
+  '';
+
   preConfigure = ''
     patchShebangs ./src/
   '';
diff --git a/pkgs/applications/science/logic/cvc4/minisat-fenv.patch b/pkgs/applications/science/logic/cvc4/minisat-fenv.patch
new file mode 100644
index 00000000000..686d5a1c5b4
--- /dev/null
+++ b/pkgs/applications/science/logic/cvc4/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
+
-- 
cgit 1.4.1