Skip to content

Commit

Permalink
Fix CMake build for Glucose Syrup
Browse files Browse the repository at this point in the history
  • Loading branch information
Matthias Güdemann committed Apr 21, 2018
1 parent 290feb4 commit aa3caa3
Show file tree
Hide file tree
Showing 2 changed files with 84 additions and 20 deletions.
102 changes: 82 additions & 20 deletions scripts/glucose-syrup-patch
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
diff -rupN glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
--- glucose-syrup/core/Solver.cc 2014-10-03 10:10:21.000000000 +0100
+++ glucose-syrup-patched/core/Solver.cc 2016-07-08 13:06:02.772186004 +0100
diff -rupNw glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
--- glucose-syrup/core/Solver.cc 2014-10-03 11:10:21.000000000 +0200
+++ glucose-syrup-patched/core/Solver.cc 2018-04-21 16:58:22.950005391 +0200
@@ -931,7 +931,6 @@ void Solver::uncheckedEnqueue(Lit p, CRe
CRef Solver::propagate() {
CRef confl = CRef_Undef;
Expand All @@ -19,9 +19,9 @@ diff -rupN glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
// Model found:
return l_True;
}
diff -rupN glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
--- glucose-syrup/core/SolverTypes.h 2014-10-03 10:10:22.000000000 +0100
+++ glucose-syrup-patched/core/SolverTypes.h 2016-07-08 13:06:02.772186004 +0100
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>
Expand All @@ -32,9 +32,20 @@ diff -rupN glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTyp

#include "mtl/IntTypes.h"
#include "mtl/Alg.h"
diff -rupN glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
--- glucose-syrup/mtl/IntTypes.h 2014-10-03 10:10:22.000000000 +0100
+++ glucose-syrup-patched/mtl/IntTypes.h 2016-07-08 13:06:02.772186004 +0100
@@ -170,7 +172,10 @@ class Clause {
unsigned lbd : BITS_LBD;
} header;

+#include <util/pragma_push.def>
+#include <util/pragma_wzero_length_array.def>
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
+#include <util/pragma_pop.def>

friend class ClauseAllocator;

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

Expand All @@ -45,10 +56,49 @@ diff -rupN glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h

#endif

diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 10:10:22.000000000 +0100
+++ glucose-syrup-patched/simp/SimpSolver.cc 2016-07-08 13:07:00.396187548 +0100
@@ -687,11 +687,11 @@ bool SimpSolver::eliminate(bool turn_off
diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
--- glucose-syrup/mtl/Vec.h 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/mtl/Vec.h 2018-04-21 16:58:22.950005391 +0200
@@ -103,7 +103,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 -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
@@ -319,10 +319,13 @@ 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:;
@@ -353,10 +356,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:;
@@ -687,11 +692,11 @@ bool SimpSolver::eliminate(bool turn_off
//

int toPerform = clauses.size()<=4800000;
Expand All @@ -62,7 +112,7 @@ diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolve
while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){

gatherTouchedClauses();
@@ -760,10 +760,11 @@ bool SimpSolver::eliminate(bool turn_off
@@ -760,10 +765,11 @@ bool SimpSolver::eliminate(bool turn_off
checkGarbage();
}

Expand All @@ -75,9 +125,21 @@ diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolve

return ok;

diff -rupN glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
--- glucose-syrup/utils/ParseUtils.h 2014-10-03 10:10:22.000000000 +0100
+++ glucose-syrup-patched/utils/ParseUtils.h 2016-07-08 13:06:02.772186004 +0100
diff -rupNw glucose-syrup/utils/Options.h glucose-syrup-patched/utils/Options.h
--- glucose-syrup/utils/Options.h 2014-10-03 11:10:22.000000000 +0200
+++ glucose-syrup-patched/utils/Options.h 2018-04-21 16:58:22.950005391 +0200
@@ -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 -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>
Expand Down Expand Up @@ -109,9 +171,9 @@ diff -rupN glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUti

int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
void operator ++ () { pos++; assureLookahead(); }
diff -rupN glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
--- glucose-syrup/utils/System.h 2014-10-03 10:10:22.000000000 +0100
+++ glucose-syrup-patched/utils/System.h 2016-07-08 13:06:02.776186005 +0100
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
Expand Down
2 changes: 2 additions & 0 deletions scripts/glucose_CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,5 @@ target_include_directories(glucose-condensed
PUBLIC
${CMAKE_CURRENT_SOURCE_DIR}
)

target_link_libraries(glucose-condensed util)

0 comments on commit aa3caa3

Please sign in to comment.