Skip to content

Commit e49a9ba

Browse files
author
Peter Schrammel
committed
Merge pull request #8 from tautschnig/minisat-build-update
Minisat build update
2 parents cd7ddc9 + 0805a35 commit e49a9ba

File tree

6 files changed

+74
-47
lines changed

6 files changed

+74
-47
lines changed

‎.travis.yml

-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ before_install:
1818
- if [ "$(expr substr $(uname -s) 1 5)" == "Linux" ] ; then sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test && sudo apt-get -qq update && sudo apt-get -qq install g++-4.8 gcc-4.8 && sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 90 && sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 90 ; fi
1919

2020
install:
21-
- chmod a+x regression/failed-tests-printer.pl
2221
- cd src && make minisat2-download
2322

2423
script:

‎scripts/minisat-2.2.0-patch renamed to ‎scripts/minisat-2.2.1-patch

+63-35
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
diff -rupN minisat-2.2.0/core/Solver.cc minisat-2.2.0.patched/core/Solver.cc
2-
--- minisat-2.2.0/core/Solver.cc 2010-07-10 17:07:36.000000000 +0100
3-
+++ minisat-2.2.0.patched/core/Solver.cc 2015-05-22 19:06:39.000000000 +0100
4-
@@ -209,7 +209,7 @@ void Solver::cancelUntil(int level) {
1+
diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/core/Solver.cc
2+
--- minisat-2.2.1/minisat/core/Solver.cc 2011-02-21 13:31:17.000000000 +0000
3+
+++ minisat-2.2.1.patched/minisat/core/Solver.cc 2016-03-05 16:21:17.000000000 +0000
4+
@@ -210,7 +210,7 @@
55
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
66
Var x = var(trail[c]);
77
assigns [x] = l_Undef;
@@ -10,7 +10,7 @@ diff -rupN minisat-2.2.0/core/Solver.cc minisat-2.2.0.patched/core/Solver.cc
1010
polarity[x] = sign(trail[c]);
1111
insertVarOrder(x); }
1212
qhead = trail_lim[level];
13-
@@ -657,7 +657,7 @@ lbool Solver::search(int nof_conflicts)
13+
@@ -666,7 +666,7 @@
1414

1515
}else{
1616
// NO CONFLICT
@@ -19,10 +19,10 @@ diff -rupN minisat-2.2.0/core/Solver.cc minisat-2.2.0.patched/core/Solver.cc
1919
// Reached bound on number of conflicts:
2020
progress_estimate = progressEstimate();
2121
cancelUntil(0);
22-
diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/SolverTypes.h
23-
--- minisat-2.2.0/core/SolverTypes.h 2010-07-10 17:07:36.000000000 +0100
24-
+++ minisat-2.2.0.patched/core/SolverTypes.h 2015-05-22 19:06:39.000000000 +0100
25-
@@ -47,7 +47,7 @@ struct Lit {
22+
diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat/core/SolverTypes.h
23+
--- minisat-2.2.1/minisat/core/SolverTypes.h 2011-02-21 13:31:17.000000000 +0000
24+
+++ minisat-2.2.1.patched/minisat/core/SolverTypes.h 2016-03-05 16:29:42.000000000 +0000
25+
@@ -47,7 +47,7 @@
2626
int x;
2727

2828
// Use this as a constructor:
@@ -31,7 +31,7 @@ diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/SolverTyp
3131

3232
bool operator == (Lit p) const { return x == p.x; }
3333
bool operator != (Lit p) const { return x != p.x; }
34-
@@ -55,7 +55,7 @@ struct Lit {
34+
@@ -55,7 +55,7 @@
3535
};
3636

3737

@@ -40,10 +40,38 @@ diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/SolverTyp
4040
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
4141
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
4242
inline bool sign (Lit p) { return p.x & 1; }
43-
diff -rupN minisat-2.2.0/mtl/IntTypes.h minisat-2.2.0.patched/mtl/IntTypes.h
44-
--- minisat-2.2.0/mtl/IntTypes.h 2010-07-10 17:07:36.000000000 +0100
45-
+++ minisat-2.2.0.patched/mtl/IntTypes.h 2015-05-22 19:06:39.000000000 +0100
46-
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
43+
@@ -142,11 +142,12 @@
44+
for (int i = 0; i < ps.size(); i++)
45+
data[i].lit = ps[i];
46+
47+
- if (header.has_extra)
48+
+ if (header.has_extra) {
49+
if (header.learnt)
50+
data[header.size].act = 0;
51+
else
52+
calcAbstraction();
53+
+ }
54+
}
55+
56+
// NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
57+
@@ -157,11 +158,12 @@
58+
for (int i = 0; i < from.size(); i++)
59+
data[i].lit = from[i];
60+
61+
- if (header.has_extra)
62+
+ if (header.has_extra) {
63+
if (header.learnt)
64+
data[header.size].act = from.data[header.size].act;
65+
else
66+
data[header.size].abs = from.data[header.size].abs;
67+
+ }
68+
}
69+
70+
public:
71+
diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl/IntTypes.h
72+
--- minisat-2.2.1/minisat/mtl/IntTypes.h 2011-02-21 13:31:17.000000000 +0000
73+
+++ minisat-2.2.1.patched/minisat/mtl/IntTypes.h 2016-03-05 16:21:17.000000000 +0000
74+
@@ -31,7 +31,9 @@
4775
#else
4876

4977
# include <stdint.h>
@@ -53,10 +81,10 @@ diff -rupN minisat-2.2.0/mtl/IntTypes.h minisat-2.2.0.patched/mtl/IntTypes.h
5381

5482
#endif
5583

56-
diff -rupN minisat-2.2.0/mtl/Vec.h minisat-2.2.0.patched/mtl/Vec.h
57-
--- minisat-2.2.0/mtl/Vec.h 2010-07-10 17:07:36.000000000 +0100
58-
+++ minisat-2.2.0.patched/mtl/Vec.h 2015-05-22 19:06:39.000000000 +0100
59-
@@ -96,7 +96,7 @@ template<class T>
84+
diff -urN minisat-2.2.1/minisat/mtl/Vec.h minisat-2.2.1.patched/minisat/mtl/Vec.h
85+
--- minisat-2.2.1/minisat/mtl/Vec.h 2011-02-21 13:31:17.000000000 +0000
86+
+++ minisat-2.2.1.patched/minisat/mtl/Vec.h 2016-03-05 16:21:17.000000000 +0000
87+
@@ -96,7 +96,7 @@
6088
void vec<T>::capacity(int min_cap) {
6189
if (cap >= min_cap) return;
6290
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
@@ -65,10 +93,10 @@ diff -rupN minisat-2.2.0/mtl/Vec.h minisat-2.2.0.patched/mtl/Vec.h
6593
throw OutOfMemoryException();
6694
}
6795

68-
diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolver.cc
69-
--- minisat-2.2.0/simp/SimpSolver.cc 2010-07-10 17:07:36.000000000 +0100
70-
+++ minisat-2.2.0.patched/simp/SimpSolver.cc 2015-06-14 22:37:51.000000000 +0100
71-
@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, b
96+
diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat/simp/SimpSolver.cc
97+
--- minisat-2.2.1/minisat/simp/SimpSolver.cc 2011-02-21 13:31:17.000000000 +0000
98+
+++ minisat-2.2.1.patched/minisat/simp/SimpSolver.cc 2016-03-05 16:21:17.000000000 +0000
99+
@@ -130,8 +130,6 @@
72100
return result;
73101
}
74102

@@ -77,7 +105,7 @@ diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolve
77105
bool SimpSolver::addClause_(vec<Lit>& ps)
78106
{
79107
#ifndef NDEBUG
80-
@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps
108+
@@ -227,10 +225,12 @@
81109
if (var(qs[i]) != v){
82110
for (int j = 0; j < ps.size(); j++)
83111
if (var(ps[j]) == var(qs[i]))
@@ -90,7 +118,7 @@ diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolve
90118
out_clause.push(qs[i]);
91119
}
92120
next:;
93-
@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps
121+
@@ -261,10 +261,12 @@
94122
if (var(__qs[i]) != v){
95123
for (int j = 0; j < ps.size(); j++)
96124
if (var(__ps[j]) == var(__qs[i]))
@@ -103,10 +131,10 @@ diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolve
103131
size++;
104132
}
105133
next:;
106-
diff -rupN minisat-2.2.0/utils/Options.h minisat-2.2.0.patched/utils/Options.h
107-
--- minisat-2.2.0/utils/Options.h 2010-07-10 17:07:36.000000000 +0100
108-
+++ minisat-2.2.0.patched/utils/Options.h 2015-06-14 22:33:24.000000000 +0100
109-
@@ -60,7 +60,7 @@ class Option
134+
diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/utils/Options.h
135+
--- minisat-2.2.1/minisat/utils/Options.h 2011-02-21 13:31:17.000000000 +0000
136+
+++ minisat-2.2.1.patched/minisat/utils/Options.h 2016-03-05 16:21:17.000000000 +0000
137+
@@ -60,7 +60,7 @@
110138
struct OptionLt {
111139
bool operator()(const Option* x, const Option* y) {
112140
int test1 = strcmp(x->category, y->category);
@@ -115,7 +143,7 @@ diff -rupN minisat-2.2.0/utils/Options.h minisat-2.2.0.patched/utils/Options.h
115143
}
116144
};
117145

118-
@@ -282,15 +282,15 @@ class Int64Option : public Option
146+
@@ -282,15 +282,15 @@
119147
if (range.begin == INT64_MIN)
120148
fprintf(stderr, "imin");
121149
else
@@ -134,10 +162,10 @@ diff -rupN minisat-2.2.0/utils/Options.h minisat-2.2.0.patched/utils/Options.h
134162
if (verbose){
135163
fprintf(stderr, "\n %s\n", description);
136164
fprintf(stderr, "\n");
137-
diff -rupN minisat-2.2.0/utils/ParseUtils.h minisat-2.2.0.patched/utils/ParseUtils.h
138-
--- minisat-2.2.0/utils/ParseUtils.h 2010-07-10 17:07:36.000000000 +0100
139-
+++ minisat-2.2.0.patched/utils/ParseUtils.h 2015-05-22 19:06:39.000000000 +0100
140-
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
165+
diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat/utils/ParseUtils.h
166+
--- minisat-2.2.1/minisat/utils/ParseUtils.h 2011-02-21 13:31:17.000000000 +0000
167+
+++ minisat-2.2.1.patched/minisat/utils/ParseUtils.h 2016-03-05 16:21:17.000000000 +0000
168+
@@ -24,7 +24,7 @@
141169
#include <stdlib.h>
142170
#include <stdio.h>
143171

@@ -146,7 +174,7 @@ diff -rupN minisat-2.2.0/utils/ParseUtils.h minisat-2.2.0.patched/utils/ParseUti
146174

147175
namespace Minisat {
148176

149-
@@ -35,7 +35,7 @@ static const int buffer_size = 1048576;
177+
@@ -35,7 +35,7 @@
150178

151179

152180
class StreamBuffer {
@@ -155,7 +183,7 @@ diff -rupN minisat-2.2.0/utils/ParseUtils.h minisat-2.2.0.patched/utils/ParseUti
155183
unsigned char buf[buffer_size];
156184
int pos;
157185
int size;
158-
@@ -43,10 +43,10 @@ class StreamBuffer {
186+
@@ -43,10 +43,10 @@
159187
void assureLookahead() {
160188
if (pos >= size) {
161189
pos = 0;

‎src/Makefile

+7-7
Original file line numberDiff line numberDiff line change
@@ -54,13 +54,13 @@ $(patsubst %, %_clean, $(DIRS)):
5454
# minisat 2 download, for your convenience
5555

5656
minisat2-download:
57-
@echo "Downloading Minisat 2.2.0"
58-
@lwp-download http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.0.orig.tar.gz
59-
@tar xfz minisat2_2.2.0.orig.tar.gz
60-
@rm -Rf ../minisat-2.2.0
61-
@mv minisat-2.2.0 ../minisat-2.2.0
62-
@(cd ../minisat-2.2.0; patch -p1 < ../scripts/minisat-2.2.0-patch)
63-
@rm minisat2_2.2.0.orig.tar.gz
57+
@echo "Downloading Minisat 2.2.1"
58+
@lwp-download http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
59+
@tar xfz minisat2_2.2.1.orig.tar.gz
60+
@rm -Rf ../minisat-2.2.1
61+
@mv minisat2-2.2.1 ../minisat-2.2.1
62+
@(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
63+
@rm minisat2_2.2.1.orig.tar.gz
6464

6565
glucose-download:
6666
@echo "Downloading glucose-syrup"

‎src/config.inc

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ BUILD_ENV = AUTO
1515
#CHAFF = ../../zChaff
1616
#BOOLEFORCE = ../../booleforce-0.4
1717
#MINISAT = ../../MiniSat-p_v1.14
18-
MINISAT2 = ../../minisat-2.2.0
18+
MINISAT2 = ../../minisat-2.2.1
1919
#GLUCOSE = ../../glucose-syrup
2020
#SMVSAT =
2121
#LIBZIPLIB = /opt/local/lib/libzip

‎src/solvers/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ endif
1717
ifneq ($(MINISAT2),)
1818
MINISAT2_SRC=sat/satcheck_minisat2.cpp
1919
MINISAT2_INCLUDE=-I $(MINISAT2)
20-
MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
20+
MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT)
2121
CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
2222
override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
2323
endif

‎src/solvers/sat/satcheck_minisat2.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ Author: Daniel Kroening, [email protected]
1717

1818
#include "satcheck_minisat2.h"
1919

20-
#include <core/Solver.h>
21-
#include <simp/SimpSolver.h>
20+
#include <minisat/core/Solver.h>
21+
#include <minisat/simp/SimpSolver.h>
2222

2323
#ifndef HAVE_MINISAT2
2424
#error "Expected HAVE_MINISAT2"

0 commit comments

Comments
 (0)