Updating CryptoMiniSat to r565. Should solve the problem with performReplace failing...

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

diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp
index 890a8ba558206ec32d3913ba6cf03c41cea0b808..36d277e2b83b15cc7cd39458868f95d373d5b1fa 100644 (file)
--- a/src/sat/cryptominisat2/ClauseCleaner.cpp
+++ b/src/sat/cryptominisat2/ClauseCleaner.cpp
@@ -119,8 +119,8 @@ void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type)
         
         if (c.size() == 2) {
             vec<Lit> ps(2);
-            ps[0] = c[0];
-            ps[1] = c[1];
+            ps[0] = c[0].unsign();
+            ps[1] = c[1].unsign();
             solver.toReplace->replace(ps, c.xor_clause_inverted(), c.group);
             solver.removeClause(c);
             s++;

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index f11cf4e08dccd4e2e9b9c9feeb3e2ab8172c9fee..e71c9c4782bca10cf2d20d61b75c1d98aad4f2a3 100644 (file)
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -79,11 +79,12 @@ void Conglomerate::fillVarToXor()
     }
 }
 
-void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vec<Lit>& vars) {
+void Conglomerate::process_clause(XorClause& x, const uint num, Var remove_var, vec<Lit>& vars) {
     for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) {
-        if (a->var() != var) {
-            vars.push(*a);
-            varToXorMap::iterator finder = varToXor.find(a->var());
+        Var var = a->var();
+        if (var != remove_var) {
+            vars.push(Lit(var, false));
+            varToXorMap::iterator finder = varToXor.find(var);
             if (finder != varToXor.end()) {
                 vector<pair<XorClause*, uint> >::iterator it =
                     std::find(finder->second.begin(), finder->second.end(), make_pair(&x, num));

diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h
index 4193fce2c018a9dc2824bca5cc896b0be9270269..d0eeb7c9b08b32d3ebee14cc5b3d238e7322afed 100644 (file)
--- a/src/sat/cryptominisat2/Conglomerate.h
+++ b/src/sat/cryptominisat2/Conglomerate.h
@@ -33,7 +33,7 @@ public:
     
 private:
     
-    void process_clause(XorClause& x, const uint num, uint var, vec<Lit>& vars);
+    void process_clause(XorClause& x, const uint num, Var remove_var, vec<Lit>& vars);
     void fillVarToXor();
     void clearDouble(vec<Lit>& ps) const;
     void clearToRemove();

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 88131767eba0d727a4a7291212a6508bd9cc67c2..d8c5a3c5a985280ee081e7b38c2a32c90ae923c9 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -376,6 +376,18 @@ void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint ori
     else            clauses_literals -= origSize;
 }
 
+void Solver::detachModifiedClause(const Var var1, const Var var2, const uint origSize, const XorClause* address)
+{
+    assert(origSize > 2);
+    
+    assert(find(xorwatches[var1], address));
+    assert(find(xorwatches[var2], address));
+    remove(xorwatches[var1], address);
+    remove(xorwatches[var2], address);
+    if (address->learnt()) learnts_literals -= origSize;
+    else            clauses_literals -= origSize;
+}
+
 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
 //
 void Solver::cancelUntil(int level)

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 3c16fde863e0e6fdb3aec7f6f9221f60acc35b4e..65a07527a764b84b2b315509aa75446c92be60e8 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -273,6 +273,7 @@ protected:
     void     detachClause     (const XorClause& c);
     void     detachClause     (const Clause& c);       // Detach a clause to watcher lists.
     void     detachModifiedClause(const Lit lit1, const Lit lit2, const uint size, const Clause* address);
+    void     detachModifiedClause(const Var var1, const Var var2, const uint origSize, const XorClause* address);
     void     removeClause(Clause& c);                  // Detach and free a clause.
     void     removeClause(XorClause& c);               // Detach and free a clause.
     bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 37711634065f150550c0efa97d55b658723545e4..b18870e316078aab5f1febe7b6eba2d70ef8b4e1 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,3 +1,3 @@
 CryptoMiniSat
-SVN revision: 561
-GIT revision: 56d0a713979afbe737a7da1670f39eaf8c6f53a5
+SVN revision: 565
+GIT revision: a83e40474c31b7a0b902addfc37ff99a188d0ad3

diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 0da1bec86b241e3826e467527f36940cba4b6abe..62d840d3f395ada3d9669e470e2952f2461f13d6 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -5,6 +5,7 @@
 #include "ClauseCleaner.h"
 
 //#define VERBOSE_DEBUG
+//#define DEBUG_REPLACER
 
 #ifdef VERBOSE_DEBUG
 #include <iostream>
@@ -42,6 +43,16 @@ void VarReplacer::performReplace()
     }
     #endif
     
+    S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses);
+    S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts);
+    S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
+    
+    S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses);
+    S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts);
+    S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
+    
+    if (!addedNewClause || replacedVars == 0) return;
+    
     uint i = 0;
     const vector<bool>& removedVars = S->conglomerate->getRemovedVars();
     for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, i++) {
@@ -50,19 +61,6 @@ void VarReplacer::performReplace()
         if (!removedVars[it->var()])
             S->setDecisionVar(it->var(), true);
     }
-
-    if (!addedNewClause || replacedVars == 0) return;
-    
-    S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses);
-    S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts);
-    S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
-    
-    S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses);
-    S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts);
-    S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
-    for (uint i = 0; i < clauses.size(); i++)
-        S->removeClause(*clauses[i]);
-    clauses.clear();
     
     replace_set(S->clauses);
     replace_set(S->learnts);
@@ -70,6 +68,10 @@ void VarReplacer::performReplace()
     replace_set(S->xorclauses, true);
     replace_set(S->conglomerate->getCalcAtFinish(), false);
     
+    for (uint i = 0; i < clauses.size(); i++)
+        S->removeClause(*clauses[i]);
+    clauses.clear();
+    
     if (S->verbosity >=1)
         printf("|  Replacing   %8d vars, replaced %8d lits                          |\n", replacedVars, replacedLits);
     
@@ -81,68 +83,29 @@ void VarReplacer::performReplace()
     S->order_heap.filter(Solver::VarFilter(*S));
 }
 
-void VarReplacer::replace_set(vec<XorClause*>& cs, const bool need_reattach)
+void VarReplacer::replace_set(vec<XorClause*>& cs, const bool isAttached)
 {
     XorClause **a = cs.getData();
     XorClause **r = a;
     for (XorClause **end = a + cs.size(); r != end;) {
         XorClause& c = **r;
         
-        bool needReattach = false;
+        bool changed = false;
+        Var origVar1 = c[0].var();
+        Var origVar2 = c[1].var();
         for (Lit *l = &c[0], *lend = l + c.size(); l != lend; l++) {
             Lit newlit = table[l->var()];
             if (newlit.var() != l->var()) {
-                if (need_reattach && !needReattach)
-                    S->detachClause(c);
-                needReattach = true;
+                changed = true;
                 *l = Lit(newlit.var(), false);
                 c.invert(newlit.sign());
                 replacedLits++;
             }
         }
         
-        if (need_reattach && needReattach) {
-            std::sort(c.getData(), c.getData() + c.size());
-            Lit p;
-            int i, j;
-            for (i = j = 0, p = lit_Undef; i < c.size(); i++) {
-                c[i] = c[i].unsign();
-                if (c[i] == p) {
-                    //added, but easily removed
-                    j--;
-                    p = lit_Undef;
-                    if (!S->assigns[c[i].var()].isUndef())
-                        c.invert(S->assigns[c[i].var()].getBool());
-                } else if (S->assigns[c[i].var()].isUndef()) //just add
-                    c[j++] = p = c[i];
-                else c.invert(S->assigns[c[i].var()].getBool()); //modify xor_clause_inverted instead of adding
-            }
-            c.shrink(i - j);
-            
-            switch (c.size()) {
-            case 0:
-                if (!c.xor_clause_inverted())
-                    S->ok = false;
-                r++;
-                break;
-            case 1:
-                S->uncheckedEnqueue(c[0] ^ c.xor_clause_inverted());
-                r++;
-                break;
-            case 2: {
-                vec<Lit> ps(2);
-                ps[0] = c[0];
-                ps[1] = c[1];
-                addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true);
-                c.mark(1);
-                r++;
-                break;
-            }
-            default:
-                S->attachClause(c);
-                *a++ = *r++;
-                break;
-            }
+        if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) {
+            c.mark(1);
+            r++;
         } else {
             *a++ = *r++;
         }
@@ -150,6 +113,56 @@ void VarReplacer::replace_set(vec<XorClause*>& cs, const bool need_reattach)
     cs.shrink(r-a);
 }
 
+const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2)
+{
+    uint origSize = c.size();
+    std::sort(c.getData(), c.getData() + c.size());
+    Lit p;
+    int i, j;
+    for (i = j = 0, p = lit_Undef; i < c.size(); i++) {
+        c[i] = c[i].unsign();
+        if (c[i] == p) {
+            //added, but easily removed
+            j--;
+            p = lit_Undef;
+            if (!S->assigns[c[i].var()].isUndef())
+                c.invert(S->assigns[c[i].var()].getBool());
+        } else if (S->assigns[c[i].var()].isUndef()) //just add
+            c[j++] = p = c[i];
+        else c.invert(S->assigns[c[i].var()].getBool()); //modify xor_clause_inverted instead of adding
+    }
+    c.shrink(i - j);
+    
+    switch (c.size()) {
+    case 0:
+        S->detachModifiedClause(origVar1, origVar2, origSize, &c);
+        if (!c.xor_clause_inverted())
+            S->ok = false;
+        return true;
+    case 1:
+        S->detachModifiedClause(origVar1, origVar2, origSize, &c);
+        S->uncheckedEnqueue(c[0] ^ c.xor_clause_inverted());
+        return true;
+    case 2: {
+        S->detachModifiedClause(origVar1, origVar2, origSize, &c);
+        vec<Lit> ps(2);
+        ps[0] = c[0];
+        ps[1] = c[1];
+        addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true);
+        return true;
+    }
+    default:
+        if (origVar1 != c[0].var() || origVar2 != c[1].var()) {
+            S->detachModifiedClause(origVar1, origVar2, origSize, &c);
+            S->attachClause(c);
+        }
+        return false;
+    }
+    
+    assert(false);
+    return false;
+}
+
 void VarReplacer::replace_set(vec<Clause*>& cs)
 {
     Clause **a = cs.getData();
@@ -177,7 +190,7 @@ void VarReplacer::replace_set(vec<Clause*>& cs)
     cs.shrink(r-a);
 }
 
-bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2)
+const bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2)
 {
     bool satisfied = false;
     std::sort(c.getData(), c.getData() + c.size());
@@ -205,8 +218,8 @@ bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit o
         S->ok = false;
         return true;
     case 1 :
-        S->uncheckedEnqueue(c[0]);
         S->detachModifiedClause(origLit1, origLit2, origSize, &c);
+        S->uncheckedEnqueue(c[0]);
         return true;
     case 2:
         S->detachModifiedClause(origLit1, origLit2, origSize, &c);
@@ -219,6 +232,9 @@ bool VarReplacer::handleUpdatedClause(Clause& c, const Lit origLit1, const Lit o
         }
         return false;
     }
+    
+    assert(false);
+    return false;
 }
 
 const uint VarReplacer::getNumReplacedLits() const
@@ -276,6 +292,19 @@ void VarReplacer::extendModel() const
 
 void VarReplacer::replace(vec<Lit>& ps, const bool xor_clause_inverted, const uint group)
 {
+    #ifdef VERBOSE_DEBUG
+    cout << "replace() called with var " << ps[0]+1 << " and var " << ps[1]+1 << " with xor_clause_inverted " << xor_clause_inverted << endl;
+    #endif
+    
+    #ifdef DEBUG_REPLACER
+    assert(ps.size() == 2);
+    assert(!ps[0].sign());
+    assert(!ps[1].sign());
+    assert(S->assigns[ps[0].var()].isUndef());
+    assert(S->assigns[ps[1].var()].isUndef());
+    #endif
+    
+    
     addBinaryXorClause(ps, xor_clause_inverted, group);
     Var var = ps[0].var();
     Lit lit = Lit(ps[1].var(), !xor_clause_inverted);
@@ -340,9 +369,12 @@ void VarReplacer::replace(vec<Lit>& ps, const bool xor_clause_inverted, const ui
 
 void VarReplacer::addBinaryXorClause(vec<Lit>& ps, const bool xor_clause_inverted, const uint group, const bool internal)
 {
+    #ifdef DEBUG_REPLACER
+    assert(!ps[0].sign());
+    assert(!ps[1].sign());
+    #endif
+    
     Clause* c;
-    ps[0] = ps[0].unsign();
-    ps[1] = ps[1].unsign();
     ps[0] ^= xor_clause_inverted;
     
     c = Clause_new(ps, group, false);

diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h
index e6c891755e1cdab3cb39df45fab30f2783c296be..67393041d392c3fbd48214f6777757dcbffe2b66 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.h
+++ b/src/sat/cryptominisat2/VarReplacer.h
@@ -35,8 +35,9 @@ class VarReplacer
     
     private:
         void replace_set(vec<Clause*>& set);
-        void replace_set(vec<XorClause*>& cs, const bool need_reattach);
-        bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2);
+        void replace_set(vec<XorClause*>& cs, const bool isAttached);
+        const bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2);
+        const bool handleUpdatedClause(XorClause& c, const Var origVar1, const Var origVar2);
         void addBinaryXorClause(vec<Lit>& ps, const bool xor_clause_inverted, const uint group, const bool internal = false);
         
         void setAllThatPointsHereTo(const Var var, const Lit lit);