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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
diff -rupN minisat-2.2.0/core/Solver.cc minisat-2.2.0.patched/core/Solver.cc
--- minisat-2.2.0/core/Solver.cc 2010-07-10 17:07:36.000000000 +0100
+++ minisat-2.2.0.patched/core/Solver.cc 2014-01-25 23:12:12.000000000 +0000
@@ -209,7 +209,7 @@ void Solver::cancelUntil(int level) {
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]);
insertVarOrder(x); }
qhead = trail_lim[level];
@@ -657,7 +657,7 @@ lbool Solver::search(int nof_conflicts)
}else{
// NO CONFLICT
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
// Reached bound on number of conflicts:
progress_estimate = progressEstimate();
cancelUntil(0);
Binary files minisat-2.2.0/core/Solver.o and minisat-2.2.0.patched/core/Solver.o differ
diff -rupN minisat-2.2.0/mtl/IntTypes.h minisat-2.2.0.patched/mtl/IntTypes.h
--- minisat-2.2.0/mtl/IntTypes.h 2010-07-10 17:07:36.000000000 +0100
+++ minisat-2.2.0.patched/mtl/IntTypes.h 2014-01-25 23:12:12.000000000 +0000
@@ -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 -rupN minisat-2.2.0/mtl/Vec.h minisat-2.2.0.patched/mtl/Vec.h
--- minisat-2.2.0/mtl/Vec.h 2010-07-10 17:07:36.000000000 +0100
+++ minisat-2.2.0.patched/mtl/Vec.h 2014-01-25 23:12:12.000000000 +0000
@@ -96,7 +96,7 @@ template<class T>
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)
+ if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
throw OutOfMemoryException();
}
diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolver.cc
--- minisat-2.2.0/simp/SimpSolver.cc 2010-07-10 17:07:36.000000000 +0100
+++ minisat-2.2.0.patched/simp/SimpSolver.cc 2014-01-25 23:18:55.000000000 +0000
@@ -130,13 +130,16 @@ lbool SimpSolver::solve_(bool do_simp, b
return result;
}
-
+#include <iostream>
bool SimpSolver::addClause_(vec<Lit>& ps)
{
#ifndef NDEBUG
for (int i = 0; i < ps.size(); i++)
+ {
+ if(isEliminated(var(ps[i]))) std::cout << "E: " << var(ps[i]) << "\n";
assert(!isEliminated(var(ps[i])));
+ }
#endif
int nclauses = clauses.size();
@@ -227,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps
if (var(qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i]))
+ {
if (ps[j] == ~qs[i])
return false;
else
goto next;
+ }
out_clause.push(qs[i]);
}
next:;
@@ -261,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps
if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(__ps[j]) == var(__qs[i]))
+ {
if (__ps[j] == ~__qs[i])
return false;
else
goto next;
+ }
size++;
}
next:;
Binary files minisat-2.2.0/simp/SimpSolver.o and minisat-2.2.0.patched/simp/SimpSolver.o differ
diff -rupN minisat-2.2.0/utils/Options.h minisat-2.2.0.patched/utils/Options.h
--- minisat-2.2.0/utils/Options.h 2010-07-10 17:07:36.000000000 +0100
+++ minisat-2.2.0.patched/utils/Options.h 2014-01-25 23:12:12.000000000 +0000
@@ -60,7 +60,7 @@ class Option
struct OptionLt {
bool operator()(const Option* x, const Option* y) {
int test1 = strcmp(x->category, y->category);
- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
}
};
diff -rupN minisat-2.2.0/utils/ParseUtils.h minisat-2.2.0.patched/utils/ParseUtils.h
--- minisat-2.2.0/utils/ParseUtils.h 2010-07-10 17:07:36.000000000 +0100
+++ minisat-2.2.0.patched/utils/ParseUtils.h 2014-01-25 23:12:12.000000000 +0000
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
#include <stdlib.h>
#include <stdio.h>
-#include <zlib.h>
+//#include <zlib.h>
namespace Minisat {
@@ -35,7 +35,7 @@ static const int buffer_size = 1048576;
class StreamBuffer {
- gzFile in;
+ //gzFile in;
unsigned char buf[buffer_size];
int pos;
int size;
@@ -43,10 +43,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(); }
|
