From f9f33b96ccdf2a06e8fad36f8c4cdb387267c8a0 Mon Sep 17 00:00:00 2001
From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 19 Apr 2010 09:38:32 +0000
Subject: [PATCH] Updating CMS2 to fix bug in Conglomerate.cpp

The Conglomeration aborted early when re-adding clauses, leading to a
bug that occured when UNSAT was found out while re-adding clauses. The
state of Conglomerate was left in a half-freed position, which lead to
Segfault when calling ~Conglomerate

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@692 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/cryptominisat2/Conglomerate.cpp | 12 ++++++++----
 src/sat/cryptominisat2/Solver.cpp       | 21 +++++++++++++++++++++
 src/sat/cryptominisat2/VERSION          |  2 +-
 3 files changed, 30 insertions(+), 5 deletions(-)

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index 683f558..1868051 100644
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -491,19 +491,23 @@ const bool Conglomerate::addRemovedClauses()
     cout << "Executing addRemovedClauses" << endl;
     #endif
     
-    for(uint i = 0; i < calcAtFinish.size(); i++)
+    for(XorClause **it = calcAtFinish.getData(), **end = calcAtFinish.getDataEnd(); it != end; it++)
     {
-        XorClause& c = *calcAtFinish[i];
+        XorClause& c = **it;
         #ifdef VERBOSE_DEBUG
         cout << "readding already removed (conglomerated) clause: ";
         c.plainPrint();
         #endif
         
-        for(Lit *l = c.getData(), *end = c.getDataEnd(); l != end ; l++)
+        for(Lit *l = c.getData(), *end2 = c.getDataEnd(); l != end2 ; l++)
             *l = l->unsign();
         
-        if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup()))
+        if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) {
+            for (;it != end; it++)
+                free(&c);
+            calcAtFinish.clear();
             return false;
+        }
         free(&c);
     }
     calcAtFinish.clear();
diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index fee91b5..4b0d541 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -1954,6 +1954,9 @@ void Solver::checkSolution()
 
 lbool Solver::solve(const vec<Lit>& assumps)
 {
+#ifdef VERBOSE_DEBUG
+    std::cout << "Solver::solve() called" << std::endl;
+#endif
     if (!ok) return l_False;
     assert(qhead == trail.size());
     
@@ -2029,6 +2032,15 @@ lbool Solver::solve(const vec<Lit>& assumps)
         delete gauss_matrixes[i];
     gauss_matrixes.clear();
 
+#ifdef VERBOSE_DEBUG
+    if (status == l_True)
+        std::cout << "Solution  is SAT" << std::endl;
+    else if (status == l_False)
+        std::cout << "Solution is UNSAT" << std::endl;
+    else
+        std::cout << "Solutions is UNKNOWN" << std::endl;
+#endif //VERBOSE_DEBUG
+
     if (status == l_True) {
         if (greedyUnbound) {
             double time = cpuTime();
@@ -2045,6 +2057,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
 #endif
         
         if (subsumer->getNumElimed() > 0 || conglomerate->needCalcAtFinish()) {
+#ifdef VERBOSE_DEBUG
+            std::cout << "Solution needs extension. Extending." << std::endl;
+#endif //VERBOSE_DEBUG
             Solver s;
             s.doSubsumption = false;
             s.performReplace = false;
@@ -2075,6 +2090,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
                 assert(status == l_True);
                 exit(-1);
             }
+#ifdef VERBOSE_DEBUG
+            std::cout << "Solution extending finished." << std::endl;
+#endif
             for (Var var = 0; var < nVars(); var++) {
                 if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False));
             }
@@ -2114,6 +2132,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
     if (doPartHandler && status != l_False) partHandler->readdRemovedClauses();
     restartTypeChooser->reset();
     
+#ifdef VERBOSE_DEBUG
+    std::cout << "Solver::solve() finished" << std::endl;
+#endif
     return status;
 }
 
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 01ed823..a01b800 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 3f1c377140a6808fe92a2126eb5ed420dfc6f051
+GIT revision: cebb0caeb2928eb96e114864c580c341e904245d
-- 
2.47.3