Updating to CMS2 r 685, fixing some bugs and doing some explicit casting on std::min

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@542 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp
index f198479fc8b61d53963c87d9528008760e4ff7b2..0509b34a4d8fe70026bdcf92374d6860eef66ecf 100644 (file)
--- a/src/sat/cryptominisat2/RestartTypeChooser.cpp
+++ b/src/sat/cryptominisat2/RestartTypeChooser.cpp
@@ -69,17 +69,18 @@ const double RestartTypeChooser::avg() const
 
 void RestartTypeChooser::calcHeap()
 {
-    firstVars.resize(topX);
+    firstVars.clear();
+    firstVars.reserve(topX);
     #ifdef VERBOSE_DEBUG
     std::cout << "First vars:" << std::endl;
     #endif
     Heap<Solver::VarOrderLt> tmp(S->order_heap);
-    uint thisTopX = std::min(S->order_heap.size(), topX);
-    for (uint i = 0; i != thisTopX; i++) {
+    uint32_t thisTopX = std::min(tmp.size(), topX);
+    for (uint32_t i = 0; i != thisTopX; i++) {
         #ifdef VERBOSE_DEBUG
         std::cout << tmp.removeMin()+1 << ", ";
         #endif
-        firstVars[i] = tmp.removeMin();
+        firstVars.push_back(tmp.removeMin());
     }
     #ifdef VERBOSE_DEBUG
     std::cout << std::endl;

diff --git a/src/sat/cryptominisat2/RestartTypeChooser.h b/src/sat/cryptominisat2/RestartTypeChooser.h
index 0ec37c391098d0835f79c1b9002016462701fb65..b328225f76c94489a8dccf8d00b079b37981cd1a 100644 (file)
--- a/src/sat/cryptominisat2/RestartTypeChooser.h
+++ b/src/sat/cryptominisat2/RestartTypeChooser.h
@@ -39,8 +39,8 @@ class RestartTypeChooser
         const double avg() const;
         
         const Solver* const S;
-        const uint topX;
-        const uint limit;
+        const uint32_t topX;
+        const uint32_t limit;
         vector<Var> sameIns;
         
         vector<Var> firstVars, firstVarsOld;

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 0a2b5c4a9af48f0ea6fa468d1640eddd6e94b288..cdc0016077b36ae98a773ac8b49a8e11cfd3102e 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -697,7 +697,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 
     seen[p.var()] = 1;
 
-    for (int i = trail.size()-1; i >= trail_lim[0]; i--) {
+    for (int32_t i = (int32_t)trail.size()-1; i >= (int32_t)trail_lim[0]; i--) {
         Var x = trail[i].var();
         if (seen[x]) {
             if (reason[x] == NULL) {
@@ -1164,6 +1164,9 @@ llbool Solver::new_decision(int& nof_conflicts, int& conflictC)
             return l_Undef;
         }
         break;
+    case auto_restart:
+        assert(false);
+        break;
     }
 
     // Simplify the set of problem clauses:

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index d4c08c2dca07657ec51754b190a66f1198afbb9f..58e2f23b076c7b6ae15c4a18325134dc33fb7e11 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -202,15 +202,15 @@ protected:
     vector<bool>        polarity;         // The preferred polarity of each variable.
     vector<bool>        decision_var;     // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
-    vec<int32_t>        trail_lim;        // Separator indices for different decision levels in 'trail'.
+    vec<uint32_t>       trail_lim;        // Separator indices for different decision levels in 'trail'.
     vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
     vec<int32_t>        level;            // 'level[var]' contains the level at which the assignment was made.
     vec<Var>            permDiff;         // LS: permDiff[var] contains the current conflict number... Used to count the number of different decision level variables in learnt clause
     #ifdef UPDATEVARACTIVITY
     vec<Lit>            lastDecisionLevel;
     #endif
-    int64_t             curRestart;
-    int64_t             conf4Stats;
+    uint64_t            curRestart;
+    uint64_t            conf4Stats;
     uint32_t            nbclausesbeforereduce;
     uint32_t            qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
     uint32_t            simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 61c0254b5e2bd2bdd6a81dcbdd6c17e58f4cc511..6421488e52d43a7cf36fffb7908333f49b04f2ab 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,3 +1,3 @@
 CryptoMiniSat
-SVN revision: 681
-GIT revision: 14117f70a8eaa1c54e813f028252fa4449fdc151
+SVN revision: 685
+GIT revision: 4c03a6cf5a46679d144b5f68cb454c1f62b0c60c