Skip to content

Fix CMake build for Glucose Syrup #2099

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 1 commit into from
Apr 23, 2018
Merged

Fix CMake build for Glucose Syrup #2099

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
102 changes: 82 additions & 20 deletions scripts/glucose-syrup-patch
View file
Open in desktop
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
Open in desktop
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)