Updating CryptoMiniSat2 to r577

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

diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp
index 36d277e2b83b15cc7cd39458868f95d373d5b1fa..e7e23cfd65a6b4ea7e7db08d6eb6bac8bfd504e3 100644 (file)
--- a/src/sat/cryptominisat2/ClauseCleaner.cpp
+++ b/src/sat/cryptominisat2/ClauseCleaner.cpp
@@ -4,6 +4,8 @@ namespace MINISAT
 {
 using namespace MINISAT;
 
+//#define DEBUG_CLEAN
+
 ClauseCleaner::ClauseCleaner(Solver& _solver) :
     solver(_solver)
 {
@@ -15,6 +17,10 @@ ClauseCleaner::ClauseCleaner(Solver& _solver) :
 
 void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type)
 {
+    #ifdef DEBUG_CLEAN
+    assert(solver.decisionLevel() == 0);
+    #endif
+    
     if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num())
         return;
     
@@ -32,6 +38,10 @@ void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type)
 
 void ClauseCleaner::removeSatisfied(vec<Clause*>& cs, ClauseSetType type)
 {
+    #ifdef DEBUG_CLEAN
+    assert(solver.decisionLevel() == 0);
+    #endif
+    
     if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num())
         return;
     
@@ -76,6 +86,10 @@ bool ClauseCleaner::cleanClause(Clause& c)
 
 void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type)
 {
+    #ifdef DEBUG_CLEAN
+    assert(solver.decisionLevel() == 0);
+    #endif
+    
     if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num())
         return;
     
@@ -92,6 +106,10 @@ void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type)
 
 void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type)
 {
+    #ifdef DEBUG_CLEAN
+    assert(solver.decisionLevel() == 0);
+    #endif
+    
     if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num())
         return;
     

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index e71c9c4782bca10cf2d20d61b75c1d98aad4f2a3..e4454f6a00e6982b8a79099e4bca7cc617a8732c 100644 (file)
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -208,6 +208,7 @@ bool Conglomerate::dealWithNewClause(vec<Lit>& ps, const bool inverted, const ui
             
             if (S->assigns[ps[0].var()] == l_Undef) {
                 assert(S->decisionLevel() == 0);
+                blocked[ps[0].var()] = true;
                 S->uncheckedEnqueue(Lit(ps[0].var(), inverted));
             } else if (S->assigns[ps[0].var()] != boolToLBool(!inverted)) {
                 #ifdef VERBOSE_DEBUG

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index d8c5a3c5a985280ee081e7b38c2a32c90ae923c9..59fda2021f82361cf4c79aa7917f02deb5678f8d 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -182,12 +182,16 @@ bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint gro
         return false;
 
     // Check if clause is satisfied and remove false/duplicate literals:
+    if (toReplace->getNumReplacedLits()) {
+        for (int i = 0; i != ps.size(); i++) {
+            ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+        }
+    }
+    
     sort(ps);
     Lit p;
     int i, j;
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
-        if (toReplace->getNumReplacedLits())
-            ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         xor_clause_inverted ^= ps[i].sign();
         ps[i] ^= ps[i].sign();
 
@@ -259,12 +263,16 @@ bool Solver::addClause(vec<Lit>& ps, const uint group, char* group_name)
         return false;
 
     // Check if clause is satisfied and remove false/duplicate literals:
+    if (toReplace->getNumReplacedLits()) {
+        for (int i = 0; i != ps.size(); i++) {
+            ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+        }
+    }
+    
     sort(ps);
     Lit p;
     int i, j;
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
-        if (toReplace->getNumReplacedLits())
-            ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         if (value(ps[i]) == l_True || ps[i] == ~p)
             return true;
         else if (value(ps[i]) != l_False && ps[i] != p)
@@ -406,7 +414,7 @@ void Solver::cancelUntil(int level)
         for (int c = trail.size()-1; c >= trail_lim[level]; c--) {
             Var     x  = trail[c].var();
             #ifdef VERBOSE_DEBUG
-            cout << "Canceling var " << x+1 << " sublevel:" << c << endl;
+            cout << "Canceling var " << x+1 << " sublevel: " << c << endl;
             #endif
             assigns[x] = l_Undef;
             insertVarOrder(x);
@@ -417,7 +425,7 @@ void Solver::cancelUntil(int level)
     }
 
     #ifdef VERBOSE_DEBUG
-    cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel:" << trail.size()-1 << ")" << endl;
+    cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel: " << trail.size()-1 << ")" << endl;
     #endif
 }
 
@@ -467,7 +475,7 @@ void Solver::set_gaussian_decision_until(const uint to)
 Lit Solver::pickBranchLit(int polarity_mode)
 {
     #ifdef VERBOSE_DEBUG
-    cout << "decision level:" << decisionLevel() << " ";
+    cout << "decision level: " << decisionLevel() << " ";
     #endif
     
     Var next = var_Undef;
@@ -521,6 +529,7 @@ Lit Solver::pickBranchLit(int polarity_mode)
     } else {
         Lit lit(next,sign);
         #ifdef VERBOSE_DEBUG
+        assert(decision_var[lit.var()]);
         cout << "decided on: " << lit.var()+1 << " to set:" << !lit.sign() << endl;
         #endif
         return lit;
@@ -740,7 +749,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 void Solver::uncheckedEnqueue(Lit p, Clause* from)
 {
     #ifdef VERBOSE_DEBUG
-    cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel:" << trail.size() << endl;
+    cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel: " << trail.size() << endl;
     #endif
     
     assert(value(p) == l_Undef);

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 65a07527a764b84b2b315509aa75446c92be60e8..d6ab797e0d5478cefe0af1dfa103e9dcec7cbf2c 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -344,7 +344,7 @@ inline void     Solver::newDecisionLevel()
 {
     trail_lim.push(trail.size());
     #ifdef VERBOSE_DEBUG
-    cout << "New decision level:" << trail_lim.size() << endl;
+    cout << "New decision level: " << trail_lim.size() << endl;
     #endif
 }
 /*inline int     Solver::nbPropagated(int level) {

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index b18870e316078aab5f1febe7b6eba2d70ef8b4e1..ddf9a023360d77bdbc48f26eba63bb6025e58945 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,3 +1,3 @@
 CryptoMiniSat
-SVN revision: 565
-GIT revision: a83e40474c31b7a0b902addfc37ff99a188d0ad3
+SVN revision: 577
+GIT revision: 2db0ff9414cbeae2c64bb74a0ec4fc2199b30c8a

diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 62d840d3f395ada3d9669e470e2952f2461f13d6..8dcabfd9a5e772791a12f983d4d12d1e5e26df80 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -19,6 +19,7 @@ namespace MINISAT
 VarReplacer::VarReplacer(Solver *_S) :
     replacedLits(0)
     , replacedVars(0)
+    , lastReplacedVars(0)
     , addedNewClause(false)
     , S(_S)
 {
@@ -34,13 +35,6 @@ void VarReplacer::performReplace()
 {
     #ifdef VERBOSE_DEBUG
     cout << "Replacer started." << endl;
-    {
-        uint i = 0;
-        for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, i++) {
-            if (it->var() == i) continue;
-            cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") <<  it->var()+1 << endl;
-        }
-    }
     #endif
     
     S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses);
@@ -51,12 +45,25 @@ void VarReplacer::performReplace()
     S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts);
     S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
     
-    if (!addedNewClause || replacedVars == 0) return;
+    if (!addedNewClause && replacedVars == lastReplacedVars) return;
+    
+    #ifdef VERBOSE_DEBUG
+    {
+        uint i = 0;
+        for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, i++) {
+            if (it->var() == i) continue;
+            cout << "Replacing var " << i+1 << " with Lit " << (it->sign() ? "-" : "") <<  it->var()+1 << endl;
+        }
+    }
+    #endif
     
     uint i = 0;
     const vector<bool>& removedVars = S->conglomerate->getRemovedVars();
     for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, i++) {
         if (it->var() == i) continue;
+        #ifdef VERBOSE_DEBUG
+        cout << "Setting var " << i+1 << " to a non-decision var" << endl;
+        #endif
         S->setDecisionVar(i, false);
         if (!removedVars[it->var()])
             S->setDecisionVar(it->var(), true);
@@ -76,6 +83,7 @@ void VarReplacer::performReplace()
         printf("|  Replacing   %8d vars, replaced %8d lits                          |\n", replacedVars, replacedLits);
     
     addedNewClause = false;
+    lastReplacedVars = replacedVars;
     
     if (S->ok)
         S->ok = (S->propagate() == NULL);
@@ -105,6 +113,7 @@ void VarReplacer::replace_set(vec<XorClause*>& cs, const bool isAttached)
         
         if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) {
             c.mark(1);
+            S->freeLater.push(&c);
             r++;
         } else {
             *a++ = *r++;
@@ -133,6 +142,11 @@ const bool VarReplacer::handleUpdatedClause(XorClause& c, const Var origVar1, co
     }
     c.shrink(i - j);
     
+    #ifdef VERBOSE_DEBUG
+    cout << "xor-clause after replacing: ";
+    c.plain_print();
+    #endif
+    
     switch (c.size()) {
     case 0:
         S->detachModifiedClause(origVar1, origVar2, origSize, &c);
@@ -293,7 +307,7 @@ 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;
+    cout << "replace() called with var " << ps[0].var()+1 << " and var " << ps[1].var()+1 << " with xor_clause_inverted " << xor_clause_inverted << endl;
     #endif
     
     #ifdef DEBUG_REPLACER

diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h
index 67393041d392c3fbd48214f6777757dcbffe2b66..a61b99b0a5f5d0ef146f4e831fc6fdb1599dd69d 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.h
+++ b/src/sat/cryptominisat2/VarReplacer.h
@@ -49,6 +49,7 @@ class VarReplacer
         
         uint replacedLits;
         uint replacedVars;
+        uint lastReplacedVars;
         bool addedNewClause;
         Solver* S;
 };

diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp
index 4490a22916b1d241605598536dcc66ba3e9b9430..c61a12d24c53b71056d9c35f6d53db8da0668f37 100644 (file)
--- a/src/sat/cryptominisat2/XorFinder.cpp
+++ b/src/sat/cryptominisat2/XorFinder.cpp
@@ -68,87 +68,6 @@ uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSiz
     return found;
 }
 
-uint XorFinder::doByPart(uint& sumLengths, const uint minSize, const uint maxSize)
-{
-    toRemove.clear();
-    toRemove.resize(cls.size(), false);
-    
-    uint sumUsage = 0;
-    vector<uint> varUsage(S->nVars(), 0);
-    for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++) {
-        const uint size = (*it)->size();
-        if ( size > maxSize || size < minSize) continue;
-        
-        for (const Lit *l = &(**it)[0], *end = l + size; l != end; l++) {
-            varUsage[l->var()]++;
-            sumUsage++;
-        }
-    }
-    
-    uint found = 0;
-    #ifdef VERBOSE_DEBUG
-    uint sumNumClauses = 0;
-    #endif
-    
-    const uint limit = 800000;
-    uint from = 0;
-    uint until = 0;
-    while (until < varUsage.size()) {
-        uint estimate = 0;
-        for (; until < varUsage.size(); until++) {
-            estimate += varUsage[until];
-            if (estimate >= limit) break;
-        }
-        #ifdef VERBOSE_DEBUG
-        printf("Xor-finding: Vars from: %d, until: %d\n", from, until);
-        uint numClauses = 0;
-        #endif
-        
-        table.clear();
-        table.reserve(estimate/2);
-        uint i = 0;
-        for (Clause **it = cls.getData(), **end = it + cls.size(); it != end; it++, i++) {
-            if (toRemove[i]) continue;
-            const uint size = (*it)->size();
-            if ( size > maxSize || size < minSize) continue;
-            
-            for (Lit *l = &(**it)[0], *end = l + size; l != end; l++) {
-                if (l->var() >= from  && l->var() <= until) {
-                    table.push_back(make_pair(*it, i));
-                    #ifdef VERBOSE_DEBUG
-                    numClauses++;
-                    #endif
-                    break;
-                }
-            }
-        }
-        #ifdef VERBOSE_DEBUG
-        printf("numClauses in range: %d\n", numClauses);
-        sumNumClauses += numClauses;
-        #endif
-        
-        uint lengths;
-        found += findXors(lengths);
-        sumLengths += lengths;
-        #ifdef VERBOSE_DEBUG
-        printf("Found in this range: %d\n", found);
-        #endif
-        
-        from = until+1;
-    }
-    
-    clearToRemove();
-    
-    if (S->ok != false)
-        S->ok = (S->propagate() == NULL);
-    
-    #ifdef VERBOSE_DEBUG
-    cout << "Overdone work due to partitioning:" << (double)sumNumClauses/(double)cls.size() << "x" << endl;
-    #endif
-    
-    return found;
-}
-
 uint XorFinder::findXors(uint& sumLengths)
 {
     #ifdef VERBOSE_DEBUG

diff --git a/src/sat/cryptominisat2/XorFinder.h b/src/sat/cryptominisat2/XorFinder.h
index 11d262494d7e5fcffe078f7ba5c86ca1b15ed588..9ba3104853b1bd935e9616dc830f717873f26f05 100644 (file)
--- a/src/sat/cryptominisat2/XorFinder.h
+++ b/src/sat/cryptominisat2/XorFinder.h
@@ -34,7 +34,6 @@ class XorFinder
     public:
         
         XorFinder(Solver* S, vec<Clause*>& cls);
-        uint doByPart(uint& sumLengths, const uint minSize, const uint maxSize);
         uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize);
         
     private: