Updating CryptoMiniSat2 to fix some minor bugs

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

diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h
index ec515fca93933baa385314d524763d3ed5b20c3f..c7faf604762647d46848b4cb608b313ea9acdbe4 100644 (file)
--- a/src/sat/cryptominisat2/Clause.h
+++ b/src/sat/cryptominisat2/Clause.h
@@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifdef _MSC_VER
 #include <msvc/stdint.h>
 #else
+#include "SmallPtr.h"
 #include <stdint.h>
 #endif //_MSC_VER
 

diff --git a/src/sat/cryptominisat2/ClauseAllocator.cpp b/src/sat/cryptominisat2/ClauseAllocator.cpp
index 826ae72329c5406dbcca8baebf60c5af4bb14a8d..f0d7fa66d61c0239e3d79da59f86c23f7fefbde7 100644 (file)
--- a/src/sat/cryptominisat2/ClauseAllocator.cpp
+++ b/src/sat/cryptominisat2/ClauseAllocator.cpp
@@ -37,6 +37,13 @@ ClauseAllocator::ClauseAllocator() :
     clausePoolBin(sizeof(Clause) + 2*sizeof(Lit))
 {}
 
+ClauseAllocator::~ClauseAllocator()
+{
+    for (uint32_t i = 0; i < dataStarts.size(); i++) {
+        free(dataStarts[i]);
+    }
+}
+
 template<class T>
 Clause* ClauseAllocator::Clause_new(const T& ps, const unsigned int group, const bool learnt)
 {

diff --git a/src/sat/cryptominisat2/ClauseAllocator.h b/src/sat/cryptominisat2/ClauseAllocator.h
index 71c479f96b75a66deff217783923892d622c10e5..db38eea0db6d792e4ec6a6f33cd240a451b5eeeb 100644 (file)
--- a/src/sat/cryptominisat2/ClauseAllocator.h
+++ b/src/sat/cryptominisat2/ClauseAllocator.h
@@ -44,6 +44,7 @@ typedef uint32_t ClauseOffset;
 class ClauseAllocator {
     public:
         ClauseAllocator();
+        ~ClauseAllocator();
         
         template<class T>
         Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index cb7ee3e82887040a3b2ab534517f4175fce98ba6..fa1d8b6dba5528f6d831e160a746d05fd5996bf1 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -2258,7 +2258,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
 #endif
         
         if (subsumer->getNumElimed() || xorSubsumer->getNumElimed()) {
-            std::cout << "c Solution needs extension. Extending." << std::endl;
+            if (verbosity >= 1) {
+                std::cout << "c Solution needs extension. Extending." << std::endl;
+            }
             Solver s;
             s.doSubsumption = false;
             s.performReplace = false;

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 75dc4448222984f3271e39e856cd017255dd82db..0e6fa532fe67f40d375e7d251e49785ffcc6b5f9 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: d1a89e619d41131629e6c4e74f9424453225ba2d
+GIT revision: fda5b5a9d05a6b2ddfa4659671d6232173c30e0e