Skip to content

Minisat build update #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 7, 2016
Merged

Minisat build update #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f4e38b8
Move to latest git version of MiniSat as Debian no longer provides th…
tautschnig Mar 5, 2016
0805a35
chmod a+x is no longer necessary
tautschnig Mar 5, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .travis.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ before_install:
- 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

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

script:
Expand Down
98 changes: 63 additions & 35 deletions scripts/minisat-2.2.0-patch → scripts/minisat-2.2.1-patch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
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 2015-05-22 19:06:39.000000000 +0100
@@ -209,7 +209,7 @@ void Solver::cancelUntil(int level) {
diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/core/Solver.cc
--- minisat-2.2.1/minisat/core/Solver.cc 2011-02-21 13:31:17.000000000 +0000
+++ minisat-2.2.1.patched/minisat/core/Solver.cc 2016-03-05 16:21:17.000000000 +0000
@@ -210,7 +210,7 @@
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
Expand All @@ -10,7 +10,7 @@ diff -rupN minisat-2.2.0/core/Solver.cc minisat-2.2.0.patched/core/Solver.cc
polarity[x] = sign(trail[c]);
insertVarOrder(x); }
qhead = trail_lim[level];
@@ -657,7 +657,7 @@ lbool Solver::search(int nof_conflicts)
@@ -666,7 +666,7 @@

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

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

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


Expand All @@ -40,10 +40,38 @@ diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/SolverTyp
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
inline bool sign (Lit p) { return p.x & 1; }
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 2015-05-22 19:06:39.000000000 +0100
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
@@ -142,11 +142,12 @@
for (int i = 0; i < ps.size(); i++)
data[i].lit = ps[i];

- if (header.has_extra)
+ if (header.has_extra) {
if (header.learnt)
data[header.size].act = 0;
else
calcAbstraction();
+ }
}

// NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
@@ -157,11 +158,12 @@
for (int i = 0; i < from.size(); i++)
data[i].lit = from[i];

- if (header.has_extra)
+ if (header.has_extra) {
if (header.learnt)
data[header.size].act = from.data[header.size].act;
else
data[header.size].abs = from.data[header.size].abs;
+ }
}

public:
diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl/IntTypes.h
--- minisat-2.2.1/minisat/mtl/IntTypes.h 2011-02-21 13:31:17.000000000 +0000
+++ minisat-2.2.1.patched/minisat/mtl/IntTypes.h 2016-03-05 16:21:17.000000000 +0000
@@ -31,7 +31,9 @@
#else

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

#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 2015-05-22 19:06:39.000000000 +0100
@@ -96,7 +96,7 @@ template<class T>
diff -urN minisat-2.2.1/minisat/mtl/Vec.h minisat-2.2.1.patched/minisat/mtl/Vec.h
--- minisat-2.2.1/minisat/mtl/Vec.h 2011-02-21 13:31:17.000000000 +0000
+++ minisat-2.2.1.patched/minisat/mtl/Vec.h 2016-03-05 16:21:17.000000000 +0000
@@ -96,7 +96,7 @@
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
Expand All @@ -65,10 +93,10 @@ diff -rupN minisat-2.2.0/mtl/Vec.h minisat-2.2.0.patched/mtl/Vec.h
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 2015-06-14 22:37:51.000000000 +0100
@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, b
diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat/simp/SimpSolver.cc
--- minisat-2.2.1/minisat/simp/SimpSolver.cc 2011-02-21 13:31:17.000000000 +0000
+++ minisat-2.2.1.patched/minisat/simp/SimpSolver.cc 2016-03-05 16:21:17.000000000 +0000
@@ -130,8 +130,6 @@
return result;
}

Expand All @@ -77,7 +105,7 @@ diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolve
bool SimpSolver::addClause_(vec<Lit>& ps)
{
#ifndef NDEBUG
@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps
@@ -227,10 +225,12 @@
if (var(qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i]))
Expand All @@ -90,7 +118,7 @@ diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolve
out_clause.push(qs[i]);
}
next:;
@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps
@@ -261,10 +261,12 @@
if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(__ps[j]) == var(__qs[i]))
Expand All @@ -103,10 +131,10 @@ diff -rupN minisat-2.2.0/simp/SimpSolver.cc minisat-2.2.0.patched/simp/SimpSolve
size++;
}
next:;
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 2015-06-14 22:33:24.000000000 +0100
@@ -60,7 +60,7 @@ class Option
diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/utils/Options.h
--- minisat-2.2.1/minisat/utils/Options.h 2011-02-21 13:31:17.000000000 +0000
+++ minisat-2.2.1.patched/minisat/utils/Options.h 2016-03-05 16:21:17.000000000 +0000
@@ -60,7 +60,7 @@
struct OptionLt {
bool operator()(const Option* x, const Option* y) {
int test1 = strcmp(x->category, y->category);
Expand All @@ -115,7 +143,7 @@ diff -rupN minisat-2.2.0/utils/Options.h minisat-2.2.0.patched/utils/Options.h
}
};

@@ -282,15 +282,15 @@ class Int64Option : public Option
@@ -282,15 +282,15 @@
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
Expand All @@ -134,10 +162,10 @@ diff -rupN minisat-2.2.0/utils/Options.h minisat-2.2.0.patched/utils/Options.h
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
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 2015-05-22 19:06:39.000000000 +0100
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat/utils/ParseUtils.h
--- minisat-2.2.1/minisat/utils/ParseUtils.h 2011-02-21 13:31:17.000000000 +0000
+++ minisat-2.2.1.patched/minisat/utils/ParseUtils.h 2016-03-05 16:21:17.000000000 +0000
@@ -24,7 +24,7 @@
#include <stdlib.h>
#include <stdio.h>

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

namespace Minisat {

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


class StreamBuffer {
Expand All @@ -155,7 +183,7 @@ diff -rupN minisat-2.2.0/utils/ParseUtils.h minisat-2.2.0.patched/utils/ParseUti
unsigned char buf[buffer_size];
int pos;
int size;
@@ -43,10 +43,10 @@ class StreamBuffer {
@@ -43,10 +43,10 @@
void assureLookahead() {
if (pos >= size) {
pos = 0;
Expand Down
14 changes: 7 additions & 7 deletions src/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,13 +54,13 @@ $(patsubst %, %_clean, $(DIRS)):
# minisat 2 download, for your convenience

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

glucose-download:
@echo "Downloading glucose-syrup"
Expand Down
2 changes: 1 addition & 1 deletion src/config.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ BUILD_ENV = AUTO
#CHAFF = ../../zChaff
#BOOLEFORCE = ../../booleforce-0.4
#MINISAT = ../../MiniSat-p_v1.14
MINISAT2 = ../../minisat-2.2.0
MINISAT2 = ../../minisat-2.2.1
#GLUCOSE = ../../glucose-syrup
#SMVSAT =
#LIBZIPLIB = /opt/local/lib/libzip
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ endif
ifneq ($(MINISAT2),)
MINISAT2_SRC=sat/satcheck_minisat2.cpp
MINISAT2_INCLUDE=-I $(MINISAT2)
MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT)
CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
endif
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/sat/satcheck_minisat2.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ Author: Daniel Kroening, [email protected]

#include "satcheck_minisat2.h"

#include <core/Solver.h>
#include <simp/SimpSolver.h>
#include <minisat/core/Solver.h>
#include <minisat/simp/SimpSolver.h>

#ifndef HAVE_MINISAT2
#error "Expected HAVE_MINISAT2"
Expand Down