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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
--- glucose-syrup/core/SolverTypes.h 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/core/SolverTypes.h 2018-04-21 16:58:22.950005391 +0200
@@ -53,7 +53,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
#include <assert.h>
#include <stdint.h>
+#ifndef _MSC_VER
#include <pthread.h>
+#endif
#include "mtl/IntTypes.h"
#include "mtl/Alg.h"
diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
--- glucose-syrup/mtl/IntTypes.h 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/mtl/IntTypes.h 2018-04-21 16:58:22.950005391 +0200
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
#else
# include <stdint.h>
+#ifndef _MSC_VER
# include <inttypes.h>
+#endif
#endif
diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
--- glucose-syrup/mtl/Vec.h
+++ glucose-syrup-patched/mtl/Vec.h
@@ -118,8 +118,10 @@
void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
- if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
- throw OutOfMemoryException();
+ if (add > INT_MAX - cap)
+ throw OutOfMemoryException();
+
+ data = (T*)xrealloc(data, (cap += add) * sizeof(T));
}
diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/simp/SimpSolver.cc 2018-04-21 16:58:22.950005391 +0200
@@ -713,11 +713,11 @@ bool SimpSolver::eliminate(bool turn_off
//
int toPerform = clauses.size()<=4800000;
-
+#if 0
if(!toPerform) {
printf("c Too many clauses... No preprocessing\n");
}
-
+#endif
while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
gatherTouchedClauses();
diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
--- glucose-syrup/utils/ParseUtils.h 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/utils/ParseUtils.h 2018-04-21 16:58:22.950005391 +0200
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
#include <stdio.h>
#include <math.h>
-#include <zlib.h>
+//#include <zlib.h>
namespace Glucose {
@@ -36,7 +36,7 @@ static const int buffer_size = 1048576;
class StreamBuffer {
- gzFile in;
+ //gzFile in;
unsigned char buf[buffer_size];
int pos;
int size;
@@ -44,10 +44,10 @@ class StreamBuffer {
void assureLookahead() {
if (pos >= size) {
pos = 0;
- size = gzread(in, buf, sizeof(buf)); } }
+ /*size = gzread(in, buf, sizeof(buf));*/ } }
public:
- explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
+ //explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
void operator ++ () { pos++; assureLookahead(); }
diff -rupNw glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
--- glucose-syrup/utils/System.h 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/utils/System.h 2018-04-21 16:58:22.950005391 +0200
@@ -60,8 +60,11 @@ static inline double Glucose::cpuTime(vo
// Laurent: I know that this will not compile directly under Windows... sorry for that
static inline double Glucose::realTime() {
+#ifndef _WIN32
struct timeval tv;
gettimeofday(&tv, NULL);
- return (double)tv.tv_sec + (double) tv.tv_usec / 1000000; }
+ return (double)tv.tv_sec + (double) tv.tv_usec / 1000000;
+#endif
+}
#endif
|
