Merge branch 'newcrypto'

updated CMS2 so that segfault will no longer happen when UNSAT is found
in the middle of a varreplacement. The clause database was left in an
undefined state, which caused ~Solver to double-free some clauses

no longer be create

Conflicts:
	src/sat/cryptominisat2/PartHandler.cpp
	src/sat/cryptominisat2/Solver.cpp
	src/sat/cryptominisat2/Solver.h
	src/sat/cryptominisat2/Subsumer.cpp
	src/sat/cryptominisat2/VERSION
	src/sat/cryptominisat2/VarReplacer.cpp
	src/sat/cryptominisat2/mtl/Vec.h

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

diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp
index 8fb97718df565e8b2fec56fa99f5abe5cfca2a7a..dddc7ff8cd2cfad50b12257f986028472ca39e71 100644 (file)
--- a/src/sat/cryptominisat2/PartHandler.cpp
+++ b/src/sat/cryptominisat2/PartHandler.cpp
@@ -276,6 +276,7 @@ void PartHandler::addSavedState()
             solver.uncheckedEnqueue(Lit(var, savedState[var] == l_False));
             assert(solver.assigns[var] == savedState[var]);
             savedState[var] = l_Undef;
+            solver.polarity[var] = (solver.assigns[var] == l_False);
         }
     }
     

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index b98ef366f179476197cf8ce6a350ceb3bbd294ae..a0f4f24c89f4cdaeccb0661ba848fc1096e1cb0d 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -82,6 +82,8 @@ Solver::Solver() :
         , doPartHandler    (true)
         , doHyperBinRes    (true)
         , doBlockedClause  (true)
+        , doVarElim        (true)
+        , doSubsume1       (true)
         , failedVarSearch  (true)
         , libraryUsage     (true)
         , greedyUnbound    (false)
@@ -140,7 +142,6 @@ Solver::~Solver()
     for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseFree(binaryClauses[i]);
     for (uint32_t i = 0; i != xorclauses.size(); i++) free(xorclauses[i]);
     clearGaussMatrixes();
-    for (uint32_t i = 0; i != freeLater.size(); i++) free(freeLater[i]);
     delete varReplacer;
     delete conglomerate;
     delete clauseCleaner;
@@ -350,6 +351,15 @@ Clause* Solver::addClauseInt(T& ps, uint group)
 template Clause* Solver::addClauseInt(Clause& ps, const uint group);
 template Clause* Solver::addClauseInt(vec<Lit>& ps, const uint group);
 
+template<class T>
+bool Solver::addClause(T& ps, const uint group, char* group_name)
+{
+    assert(decisionLevel() == 0);
+    if (ps.size() > (0x01UL << 18)) {
+        std::cout << "Too long clause!" << std::endl;
+        exit(-1);
+    }
+    
 template<class T>
 bool Solver::addClause(T& ps, const uint group, char* group_name)
 {
@@ -1021,6 +1031,7 @@ Clause* Solver::propagate(const bool update)
                     confl = k->clause;
                     //goto EndPropagate;
                 }
+                }
             }
         }
         if (confl != NULL)
@@ -1325,6 +1336,14 @@ void Solver::dumpSortedLearnts(const char* file, const uint32_t maxSize)
         }
     }
     
+    fprintf(outfile, "c clauses from binaryClauses\n");
+    if (maxSize >= 2) {
+        for (uint i = 0; i != binaryClauses.size(); i++) {
+            if (binaryClauses[i]->learnt())
+                binaryClauses[i]->plainPrint(outfile);
+        }
+    }
+    
     fprintf(outfile, "c clauses from learnts\n");
     std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
     for (int i = learnts.size()-1; i >= 0 ; i--) {
@@ -1407,6 +1426,8 @@ lbool Solver::simplify()
         lastNbBin = nbBin;
         becameBinary = 0;
     }
+    if (performReplace && varReplacer->performReplace() == false)
+        return l_False;
 
     // Remove satisfied clauses:
     clauseCleaner->removeAndCleanAll();
@@ -1945,11 +1966,11 @@ lbool Solver::solve(const vec<Lit>& assumps)
     assumps.copyTo(assumptions);
 
     int  nof_conflicts = restart_first;
-    int  nof_conflicts_fullrestart = (double)restart_first * (double)FULLRESTART_MULTIPLIER;
+    int  nof_conflicts_fullrestart = (double)restart_first * (double)FULLRESTART_MULTIPLIER + conflicts;
     //nof_conflicts_fullrestart = -1;
     uint    lastFullRestart  = starts;
     lbool   status        = l_Undef;
-    uint64_t nextSimplify = 30000;
+    uint64_t nextSimplify = 30000 + conflicts;
     
     if (nClauses() * learntsize_factor < nbclausesbeforereduce) {
         if (nClauses() * learntsize_factor < nbclausesbeforereduce/2)
@@ -1998,9 +2019,6 @@ lbool Solver::solve(const vec<Lit>& assumps)
     for (uint i = 0; i < gauss_matrixes.size(); i++)
         delete gauss_matrixes[i];
     gauss_matrixes.clear();
-    for (uint i = 0; i < freeLater.size(); i++)
-        free(freeLater[i]);
-    freeLater.clear();
 
     if (status == l_True) {
         if (greedyUnbound) {
@@ -2075,6 +2093,7 @@ lbool Solver::solve(const vec<Lit>& assumps)
 
     cancelUntil(0);
     if (doPartHandler && status != l_False) partHandler->readdRemovedClauses();
+    restartTypeChooser->reset();
     
     return status;
 }

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 3cab2f9c1abe425ca936e8e15d3d44ba4302de7f..a39ea993dacf8e8c1eb2c1290108f6170f4d0011 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -138,6 +138,8 @@ public:
     bool      doPartHandler;        // Should try to subsume clauses
     bool      doHyperBinRes;        // Should try carry out hyper-binary resolution
     bool      doBlockedClause;      // Should try to remove blocked clauses
+    bool      doVarElim;            // Perform variable elimination
+    bool      doSubsume1;           // Perform clause contraction through resolution
     bool      failedVarSearch;      // Should search for failed vars and doulbly propagated vars
     bool      libraryUsage;         // Set true if not used as a library
     bool      sateliteUsed;         // whether satielite was used on CNF before calling
@@ -213,7 +215,6 @@ protected:
     vec<Clause*>        binaryClauses;    // Binary clauses are regularly moved here
     vec<XorClause*>     xorclauses;       // List of problem xor-clauses. Will be freed
     vec<Clause*>        learnts;          // List of learnt clauses.
-    vec<XorClause*>     freeLater;        // List of xorclauses to free at the end (due to matrixes, they cannot be freed immediately)
     vec<double>         activity;         // A heuristic measurement of the activity of a variable.
     double              var_inc;          // Amount to bump next variable with.
     vec<vec<Watched> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
@@ -300,8 +301,8 @@ protected:
     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.
+    template<class T>
+    void     removeClause(T& 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.
     void     reverse_binary_clause(Clause& c) const;   // Binary clauses --- the first Lit has to be true
 
@@ -563,16 +564,20 @@ inline void Solver::reverse_binary_clause(Clause& c) const {
     }
 }*/
 
-inline void Solver::removeClause(Clause& c)
+        }
+        if (final)
+            c[0] = c[0].unsign() ^ !assigns[c[0].var()].getBool();
+        
+        c.setUpdateNeeded(false);
+    }
+}*/
+
+template<class T>
+inline void Solver::removeClause(T& c)
 {
     detachClause(c);
     clauseFree(&c);
 }
-inline void Solver::removeClause(XorClause& c)
-{
-    detachClause(c);
-    freeLater.push(&c);
-}
 
 
 //=================================================================================================

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index 0295fd8f7431147e427ff40023ac553c81519b22..29b041933c6acdcd2efc457c0a37fd7182cdf1e7 100644 (file)
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -825,10 +825,14 @@ const bool Subsumer::simplifyBySubsumption()
     else
         numMaxSubsume0 = 2000000 * (1+numCalls/2);
     
-    if (clauses.size() > 3500000)
-        numMaxSubsume1 = 100000 * (1+numCalls/2);
-    else
-        numMaxSubsume1 = 500000 * (1+numCalls/2);
+    if (solver.doSubsume1) {
+        if (clauses.size() > 3500000)
+            numMaxSubsume1 = 100000 * (1+numCalls/2);
+        else
+            numMaxSubsume1 = 500000 * (1+numCalls/2);
+    } else {
+        numMaxSubsume1 = 0;
+    }
     
     if (clauses.size() > 3500000)
         numMaxElim = (uint32_t)((double)solver.order_heap.size() / 5.0 * (0.8+(double)(numCalls)/4.0));
@@ -913,6 +917,11 @@ const bool Subsumer::simplifyBySubsumption()
         
         #ifdef BIT_MORE_VERBOSITY
         std::cout << "c time until the end of almost_all/smaller: " << cpuTime() - myTime << std::endl;
+        #endif
+        
+        if (!solver.doVarElim) break;
+        
+        #ifdef BIT_MORE_VERBOSITY
         printf("c VARIABLE ELIMINIATION\n");
         std::cout << "c  toucheds list size:" << touched_list.size() << std::endl;
         #endif

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 9f06d3b49ba0599c204751a7508eef80a2552ee3..aaf632c3ddff62d44804981134419363d845ac4e 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: e2b5fe1abd1777f753c775026d905a10006ce79b
+GIT revision: 7aa24081ccebef355347957349c09b0c00fe5512

diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 6a23e22652632020c28abb03f0d44542e5ea9708..9e36ca39932d8097329165fb0af03c5c642fb84b 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -151,7 +151,7 @@ const bool VarReplacer::replace_set(vec<XorClause*>& cs, const bool isAttached)
 {
     XorClause **a = cs.getData();
     XorClause **r = a;
-    for (XorClause **end = a + cs.size(); r != end;) {
+    for (XorClause **end = a + cs.size(); r != end; r++) {
         XorClause& c = **r;
         
         bool changed = false;
@@ -169,11 +169,14 @@ const bool VarReplacer::replace_set(vec<XorClause*>& cs, const bool isAttached)
         }
         
         if (isAttached && changed && handleUpdatedClause(c, origVar1, origVar2)) {
-            if (solver.ok == false) return false;
-            solver.freeLater.push(&c);
-            r++;
+            if (solver.ok == false) {
+                for(;r != end; r++)
+                    free(*r);
+                cs.shrink(r-a);
+                return false;
+            }
         } else {
-            *a++ = *r++;
+            *a++ = *r;
         }
     }
     cs.shrink(r-a);
@@ -240,7 +243,7 @@ const bool VarReplacer::replace_set(vec<Clause*>& cs)
 {
     Clause **a = cs.getData();
     Clause **r = a;
-    for (Clause **end = a + cs.size(); r != end; ) {
+    for (Clause **end = a + cs.size(); r != end; r++) {
         Clause& c = **r;
         bool changed = false;
         Lit origLit1 = c[0];
@@ -255,11 +258,14 @@ const bool VarReplacer::replace_set(vec<Clause*>& cs)
         }
         
         if (changed && handleUpdatedClause(c, origLit1, origLit2)) {
-            if (solver.ok == false) return false;
-            clauseFree(&c);
-            r++;
+            if (solver.ok == false) {
+                for(;r != end; r++)
+                    free(*r);
+                cs.shrink(r-a);
+                return false;
+            }
         } else {
-            *a++ = *r++;
+            *a++ = *r;
         }
     }
     cs.shrink(r-a);

diff --git a/src/sat/cryptominisat2/mtl/Vec.h b/src/sat/cryptominisat2/mtl/Vec.h
index 1c6c1aedaf229e91cd3cecfbfbd404c52bedabf5..560f0a139645dcc4fcc3f0613babee8848d81ebf 100644 (file)
--- a/src/sat/cryptominisat2/mtl/Vec.h
+++ b/src/sat/cryptominisat2/mtl/Vec.h
@@ -88,7 +88,7 @@ public:
     void     capacity (uint32_t size) { grow(size); }
 
     // Stack interface:
-    void     reserve(uint32_t res)     { if (cap < res) {cap = res; data = (T*)realloc(data, cap * sizeof(T));}}
+    void     reserve(uint32_t res)     { grow(res);}
     void     push  (void)              { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
     void     push  (const T& elem)     { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
     void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }