replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
diffblue-cbmc/scripts/minisat-2.2.1-patch

230 lines
8.1 KiB
Plaintext
Raw Blame History

diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
index 501393d..b450b73 100644
--- a/minisat/core/Solver.cc
+++ b/minisat/core/Solver.cc
@@ -210,7 +210,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];
@@ -666,7 +666,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);
diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h
index 4757b20..c3fae2b 100644
--- a/minisat/core/SolverTypes.h
+++ b/minisat/core/SolverTypes.h
@@ -47,7 +47,7 @@ struct Lit {
int x;
// Use this as a constructor:
- friend Lit mkLit(Var var, bool sign = false);
+ //friend Lit mkLit(Var var, bool sign = false);
bool operator == (Lit p) const { return x == p.x; }
bool operator != (Lit p) const { return x != p.x; }
@@ -55,7 +55,7 @@ struct Lit {
};
-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
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; }
@@ -127,7 +127,10 @@ class Clause {
unsigned has_extra : 1;
unsigned reloced : 1;
unsigned size : 27; } 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;
@@ -142,11 +145,12 @@ class Clause {
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 +161,12 @@ class Clause {
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 --git a/minisat/mtl/IntTypes.h b/minisat/mtl/IntTypes.h
index c488162..e8e24bd 100644
--- a/minisat/mtl/IntTypes.h
+++ b/minisat/mtl/IntTypes.h
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#else
# include <stdint.h>
+#ifndef _MSC_VER
# include <inttypes.h>
+#endif
#endif
diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
index b225911..d46e169 100644
--- a/minisat/mtl/Vec.h
+++ b/minisat/mtl/Vec.h
@@ -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 --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc
index 1d219a3..5ccdb67 100644
--- a/minisat/simp/SimpSolver.cc
+++ b/minisat/simp/SimpSolver.cc
@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
return result;
}
-
-
bool SimpSolver::addClause_(vec<Lit>& ps)
{
#ifndef NDEBUG
@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
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 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
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:;
diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h
index 2dba10f..7d2e83a 100644
--- a/minisat/utils/Options.h
+++ b/minisat/utils/Options.h
@@ -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);
}
};
@@ -282,15 +282,15 @@ class Int64Option : public Option
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
- fprintf(stderr, "%4"PRIi64, range.begin);
+ fprintf(stderr, "%4" PRIi64, range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
- fprintf(stderr, "%4"PRIi64, range.end);
+ fprintf(stderr, "%4" PRIi64, range.end);
- fprintf(stderr, "] (default: %"PRIi64")\n", value);
+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
diff --git a/minisat/utils/ParseUtils.h b/minisat/utils/ParseUtils.h
index d307164..7b46f09 100644
--- a/minisat/utils/ParseUtils.h
+++ b/minisat/utils/ParseUtils.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#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(); }
diff --git a/minisat/utils/System.h b/minisat/utils/System.h
index 9cbbc51..27b9700 100644
--- a/minisat/utils/System.h
+++ b/minisat/utils/System.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef Minisat_System_h
#define Minisat_System_h
-#if defined(__linux__)
+#if defined(__linux__) && defined(__GLIBC__)
#include <fpu_control.h>
#endif
Reference in New Issue View Git Blame Copy Permalink