1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
--- a/src/prop/bvminisat/simp/Main.cc 2024-05-20 14:52:26.827202665 +0200
+++ b/src/prop/bvminisat/simp/Main.cc 2024-05-20 14:53:05.967758613 +0200
@@ -80,11 +80,6 @@
setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// 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);
- printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
--- a/src/prop/bvminisat/core/Main.cc 2024-05-20 14:52:35.361105845 +0200
+++ b/src/prop/bvminisat/core/Main.cc 2024-05-20 14:53:27.116518689 +0200
@@ -80,11 +80,6 @@
setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// 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);
- printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
--- a/src/prop/minisat/simp/Main.cc 2024-05-20 14:52:44.044007338 +0200
+++ b/src/prop/minisat/simp/Main.cc 2024-05-20 14:53:39.356379840 +0200
@@ -81,11 +81,6 @@
setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// 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);
- printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
--- a/src/prop/minisat/core/Main.cc 2024-05-20 14:52:50.063939036 +0200
+++ b/src/prop/minisat/core/Main.cc 2024-05-20 14:53:53.834215599 +0200
@@ -79,11 +79,6 @@
setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// 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);
- printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
--- a/src/prop/bvminisat/utils/System.h 2024-05-20 14:54:23.301881326 +0200
+++ b/src/prop/bvminisat/utils/System.h 2024-05-20 14:54:42.030668881 +0200
@@ -21,9 +21,6 @@
#ifndef BVMinisat_System_h
#define BVMinisat_System_h
-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
#include "prop/bvminisat/mtl/IntTypes.h"
--- a/src/prop/minisat/utils/System.h 2024-05-20 14:54:28.650820656 +0200
+++ b/src/prop/minisat/utils/System.h 2024-05-20 14:54:55.435516829 +0200
@@ -21,9 +21,6 @@
#ifndef Minisat_System_h
#define Minisat_System_h
-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
#include "prop/minisat/mtl/IntTypes.h"
|
