From 56e23a7cb6425395408933e93f0f7d5285cedbe5 Mon Sep 17 00:00:00 2001 From: msoos Date: Thu, 24 Dec 2009 15:04:04 +0000 Subject: [PATCH] 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 --- src/sat/cryptominisat2/RestartTypeChooser.cpp | 9 +++++---- src/sat/cryptominisat2/RestartTypeChooser.h | 4 ++-- src/sat/cryptominisat2/Solver.cpp | 5 ++++- src/sat/cryptominisat2/Solver.h | 6 +++--- src/sat/cryptominisat2/VERSION | 4 ++-- 5 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp index f198479..0509b34 100644 --- 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 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 0ec37c3..b328225 100644 --- 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 sameIns; vector firstVars, firstVarsOld; diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 0a2b5c4..cdc0016 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -697,7 +697,7 @@ void Solver::analyzeFinal(Lit p, vec& 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 d4c08c2..58e2f23 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -202,15 +202,15 @@ protected: vector polarity; // The preferred polarity of each variable. vector decision_var; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. - vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec trail_lim; // Separator indices for different decision levels in 'trail'. vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. vec level; // 'level[var]' contains the level at which the assignment was made. vec 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 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 61c0254..6421488 100644 --- 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 -- 2.47.3