Updating CMS2 to fix some bugs

* Conglomerate was freeing the same clause. Fixed.
* Gaussian elimination is now disabled (was broken)
* Some code cleanup
* After solution extension, propagate was not called when decisionLevel
  was 0. This lead to assertion failure when adding clause during
  library usage

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

diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp
index d147e170ae6946ed97f8b9ebf327bbd401c6c519..e9d5479dc12c4565b3bb3eae1ea2efac1420d653 100644 (file)
--- a/src/sat/cryptominisat2/ClauseCleaner.cpp
+++ b/src/sat/cryptominisat2/ClauseCleaner.cpp
@@ -46,14 +46,14 @@ void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type, con
     if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num())
         return;
     
-    int i,j;
+    uint32_t i,j;
     for (i = j = 0; i < cs.size(); i++) {
         if (satisfied(*cs[i]))
             solver.removeClause(*cs[i]);
         else
             cs[j++] = cs[i];
     }
-    cs.shrink_(i - j);
+    cs.shrink(i - j);
     
     lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
 }

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index 770c88acfe0612b3e65411aac53918238f4ac229..96855d79a6b2aedc28d0266b78712478ddfd8e57 100644 (file)
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -505,8 +505,7 @@ const bool Conglomerate::addRemovedClauses()
         FILE* backup_libraryCNFfile = solver.libraryCNFFile;
         solver.libraryCNFFile = NULL;
         if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) {
-            for (;it != end; it++)
-                free(&c);
+            for (;it != end; it++) free(*it);
             calcAtFinish.clear();
             return false;
         }

diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp
index 171f9c7d202893bbf8b8e91d672356bf0b12d78a..da5f5ad23ef2cf19277777af3cf187d4c0f2a0d3 100644 (file)
--- a/src/sat/cryptominisat2/FailedVarSearcher.cpp
+++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp
@@ -304,7 +304,7 @@ end:
     
     if (solver.ok && (numFailed || goodBothSame)) {
         double time = cpuTime();
-        if ((int)origHeapSize - (int)solver.order_heap.size() >  origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) {
+        if ((int)origHeapSize - (int)solver.order_heap.size() >  (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) {
             solver.clauses_literals = 0;
             solver.learnts_literals = 0;
             for (uint32_t i = 0; i < solver.nVars(); i++) {

diff --git a/src/sat/cryptominisat2/FindUndef.cpp b/src/sat/cryptominisat2/FindUndef.cpp
index 4e35dc1cf9ce4ad8749973c2e5e1783e1da9bdba..836dc6b3740a7e0ff5b6358242a6493be7bc95f4 100644 (file)
--- a/src/sat/cryptominisat2/FindUndef.cpp
+++ b/src/sat/cryptominisat2/FindUndef.cpp
@@ -36,7 +36,7 @@ void FindUndef::fillPotential()
     int trail = solver.decisionLevel()-1;
     
     while(trail > 0) {
-        assert(trail < solver.trail_lim.size());
+        assert(trail < (int)solver.trail_lim.size());
         uint at = solver.trail_lim[trail];
         
         assert(at > 0);

diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp
index 441b4a09aa95d5724e96c768376799281d47bb63..d7deda8d557cf71bbe0e0c0db77c0aa7260a14a3 100644 (file)
--- a/src/sat/cryptominisat2/Logger.cpp
+++ b/src/sat/cryptominisat2/Logger.cpp
@@ -759,13 +759,16 @@ void Logger::printstats() const
     print_assign_var_order();
     print_branch_depth_distrib();
     print_learnt_clause_distrib();
+    #ifdef USE_GAUSS
     print_matrix_stats();
+    #endif //USE_GAUSS
     print_learnt_unitaries(0," Unitary clauses learnt until now");
     print_learnt_unitaries(last_unitary_learnt_clauses, " Unitary clauses during this restart");
     print_advanced_stats();
     print_general_stats();
 }
 
+#ifdef USE_GAUSS
 void Logger::print_matrix_stats() const
 {
     print_footer();
@@ -795,6 +798,7 @@ void Logger::print_matrix_stats() const
     
     print_footer();
 }
+#endif //USE_GAUSS
 
 void Logger::print_advanced_stats() const
 {

diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile
index 8315c2911ec98972d196a6cd516a877ba11db692..0118702da63768668ae3e468af3960000ee48868 100644 (file)
--- a/src/sat/cryptominisat2/Makefile
+++ b/src/sat/cryptominisat2/Makefile
@@ -3,7 +3,7 @@ include $(TOP)/scripts/Makefile.common
 
 MTL       = mtl
 MTRAND    = MTRand
-SOURCES   = Logger.cpp Solver.cpp Gaussian.cpp PackedRow.cpp XorFinder.cpp Conglomerate.cpp MatrixFinder.cpp VarReplacer.cpp FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp Clause.cpp FailedVarSearcher.cpp PartFinder.cpp Subsumer.cpp PartHandler.cpp XorSubsumer.cpp
+SOURCES   = Logger.cpp Solver.cpp PackedRow.cpp XorFinder.cpp Conglomerate.cpp VarReplacer.cpp FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp Clause.cpp FailedVarSearcher.cpp PartFinder.cpp Subsumer.cpp PartHandler.cpp XorSubsumer.cpp
 OBJECTS   = $(SOURCES:.cpp=.o)
 LIB       = libminisat.a
 CFLAGS    += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 4b0d541c70c2a8cd8976286edab4ea7b42a73038..b08fb5c669cf8565038d3f80d22664633867b7a4 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -32,8 +32,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "VarReplacer.h"
 #include "FindUndef.h"
-#include "Gaussian.h"
-#include "MatrixFinder.h"
 #include "Conglomerate.h"
 #include "XorFinder.h"
 #include "ClauseCleaner.h"
@@ -43,6 +41,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "PartHandler.h"
 #include "XorSubsumer.h"
 
+#ifdef USE_GAUSS
+#include "Gaussian.h"
+#include "MatrixFinder.h"
+#endif //USE_GAUSS
+
 #ifdef _MSC_VER
 #define __builtin_prefetch(a,b,c)
 //#define __builtin_prefetch(a,b)
@@ -143,7 +146,9 @@ Solver::~Solver()
     for (uint32_t i = 0; i != clauses.size(); i++) clauseFree(clauses[i]);
     for (uint32_t i = 0; i != binaryClauses.size(); i++) clauseFree(binaryClauses[i]);
     for (uint32_t i = 0; i != xorclauses.size(); i++) free(xorclauses[i]);
+    #ifdef USE_GAUSS
     clearGaussMatrixes();
+    #endif
     delete varReplacer;
     delete conglomerate;
     delete clauseCleaner;
@@ -509,9 +514,10 @@ void Solver::cancelUntil(int level)
     
     if (decisionLevel() > level) {
         
+        #ifdef USE_GAUSS
         for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++)
             (*gauss)->canceling(trail_lim[level]);
-        
+        #endif //USE_GAUSS
         
         for (int c = trail.size()-1; c >= (int)trail_lim[level]; c--) {
             Var     x  = trail[c].var();
@@ -542,12 +548,14 @@ void Solver::needLibraryCNFFile(const char* fileName)
     assert(libraryCNFFile != NULL);
 }
 
+#ifdef USE_GAUSS
 void Solver::clearGaussMatrixes()
 {
     for (uint i = 0; i < gauss_matrixes.size(); i++)
         delete gauss_matrixes[i];
     gauss_matrixes.clear();
 }
+#endif //USE_GAUSS
 
 inline bool Solver::defaultPolarity()
 {
@@ -1478,10 +1486,12 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo
     else
         dynStarts++;
     
+    #ifdef USE_GAUSS
     for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) {
         ret = (*gauss)->full_init();
         if (ret != l_Nothing) return ret;
     }
+    #endif //USE_GAUSS
 
     for (;;) {
         Clause* confl = propagate(update);
@@ -1490,6 +1500,7 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo
             ret = handle_conflict(learnt_clause, confl, conflictC, update);
             if (ret != l_Nothing) return ret;
         } else {
+            #ifdef USE_GAUSS
             bool at_least_one_continue = false;
             for (vector<Gaussian*>::iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) {
                 ret = (*gauss)->find_truths(learnt_clause, conflictC);
@@ -1497,6 +1508,7 @@ lbool Solver::search(int nof_conflicts, int nof_conflicts_fullrestart, const boo
                 else if (ret != l_Nothing) return ret;
             }
             if (at_least_one_continue) continue;
+            #endif //USE_GAUSS
             ret = new_decision(nof_conflicts, nof_conflicts_fullrestart, conflictC);
             if (ret != l_Nothing) return ret;
         }
@@ -1698,6 +1710,7 @@ double Solver::progressEstimate() const
     return progress / nVars();
 }
 
+#ifdef USE_GAUSS
 void Solver::print_gauss_sum_stats() const
 {
     if (gauss_matrixes.size() == 0) {
@@ -1726,6 +1739,7 @@ void Solver::print_gauss_sum_stats() const
         printf(" %3.0lf%% |\n", 100.0-(double)disabled/(double)gauss_matrixes.size()*100.0);
     }
 }
+#endif //USE_GAUSS
 
 inline void Solver::chooseRestartType(const uint& lastFullRestart)
 {
@@ -1752,7 +1766,8 @@ inline void Solver::chooseRestartType(const uint& lastFullRestart)
                 lastSelectedRestartType = static_restart;
                 if (verbosity >= 2)
                     printf("c |                            Decided on static restart strategy                         |\n");
-                                
+                
+                #ifdef USE_GAUSS
                 if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) {
                     double time = cpuTime();
                     MatrixFinder m(*this);
@@ -1760,6 +1775,7 @@ inline void Solver::chooseRestartType(const uint& lastFullRestart)
                     if (verbosity >=1)
                         printf("c |  Finding matrixes :    %4.2lf s (found  %5d)                                |\n", cpuTime()-time, numMatrixes);
                 }
+                #endif //USE_GAUSS
             }
             restartType = tmp;
             restartTypeChooser->reset();
@@ -1867,7 +1883,9 @@ end:
 const bool Solver::checkFullRestart(int& nof_conflicts, int& nof_conflicts_fullrestart, uint& lastFullRestart)
 {
     if (nof_conflicts_fullrestart > 0 && conflicts >= nof_conflicts_fullrestart) {
+        #ifdef USE_GAUSS
         clearGaussMatrixes();
+        #endif //USE_GAUSS
         if (verbosity >= 2)
             printf("c |                                      Fully restarting                                 |\n");
         nof_conflicts = restart_first + (double)restart_first*restart_inc;
@@ -1906,7 +1924,6 @@ inline void Solver::performStepsBeforeSolve()
         && !subsumer->simplifyBySubsumption())
         return;
     
-    const uint32_t lastReplacedVars = varReplacer->getNumReplacedVars();
     if (findBinaryXors && binaryClauses.size() < MAX_CLAUSENUM_XORFIND) {
         XorFinder xorFinder(this, binaryClauses, ClauseCleaner::binaryClauses);
         if (!xorFinder.doNoPart(2, 2)) return;
@@ -1916,7 +1933,7 @@ inline void Solver::performStepsBeforeSolve()
     
     if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) {
         XorFinder xorFinder(this, clauses, ClauseCleaner::clauses);
-        if (!xorFinder.doNoPart(3, 10)) return;
+        if (!xorFinder.doNoPart(3, 7)) return;
     }
         
     if (xorclauses.size() > 1) {
@@ -1965,7 +1982,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
     
     model.clear();
     conflict.clear();
+    #ifdef USE_GAUSS
     clearGaussMatrixes();
+    #endif //USE_GAUSS
     setDefaultRestartType();
     totalSumOfDecisionLevel = 0;
     conflictsAtLastSolve = conflicts;
@@ -2028,9 +2047,11 @@ lbool Solver::solve(const vec<Lit>& assumps)
     }
     printEndSearchStat();
     
+    #ifdef USE_GAUSS
     for (uint i = 0; i < gauss_matrixes.size(); i++)
         delete gauss_matrixes[i];
     gauss_matrixes.clear();
+    #endif //USE_GAUSS
 
 #ifdef VERBOSE_DEBUG
     if (status == l_True)
@@ -2096,6 +2117,12 @@ lbool Solver::solve(const vec<Lit>& assumps)
             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));
             }
+            ok = (propagate() == NULL);
+            if (!ok) {
+                printf("c ERROR! Extension of model failed!\n");
+                assert(ok);
+                exit(-1);
+            }
         }
 #ifndef NDEBUG
         //checkSolution();
@@ -2103,7 +2130,6 @@ lbool Solver::solve(const vec<Lit>& assumps)
         //Copy model:
         model.growTo(nVars());
         for (Var var = 0; var != nVars(); var++) model[var] = value(var);
-    
     }
     
     if (status == l_False) {
@@ -2248,8 +2274,12 @@ void Solver::printRestartStat() const
     #else
     if (verbosity >= 2) {
     #endif
-    printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart+nbCompensateSubsumer), (int)nLearnts(), (double)learnts_literals/nLearnts());
+        printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart+nbCompensateSubsumer), (int)nLearnts(), (double)learnts_literals/nLearnts());
+        #ifdef USE_GAUSS
         print_gauss_sum_stats();
+        #else //USE_GAUSS
+        printf("                    |\n");
+        #endif //USE_GAUSS
     }
 }
 
@@ -2261,7 +2291,11 @@ void Solver::printEndSearchStat() const
         if (verbosity >= 1) {
             #endif
             printf("c ====================================================================");
+            #ifdef USE_GAUSS
             print_gauss_sum_stats();
+            #else //USE_GAUSS
+            printf("\n");
+            #endif //USE_GAUSS
         }
 }
 

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 9fcda6aecae4d3e21427cc12badbf6a5ef1c0e25..66010b6443261e235d8b44fc24a1960ef7dc9895 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -38,10 +38,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "MersenneTwister.h"
 #include "SolverTypes.h"
 #include "Clause.h"
-#include "GaussianConfig.h"
 #include "Logger.h"
 #include "constants.h"
 #include "BoundedQueue.h"
+#include "GaussianConfig.h"
 
 namespace MINISAT
 {
@@ -157,6 +157,7 @@ public:
     bool      greedyUnbound;        //If set, then variables will be greedily unbounded (set to l_Undef)
     RestartType fixRestartType;     // If set, the solver will always choose the given restart strategy
     GaussianConfig gaussconfig;
+    
 
     enum { polarity_true = 0, polarity_false = 1, polarity_rnd = 3, polarity_auto = 4, polarity_manual = 5};
 
@@ -179,9 +180,11 @@ public:
     void needLibraryCNFFile(const char* fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file.
 
 protected:
-    vector<Gaussian*> gauss_matrixes;
+    #ifdef USE_GAUSS
     void print_gauss_sum_stats() const;
     void clearGaussMatrixes();
+    vector<Gaussian*> gauss_matrixes;
+    #endif //USE_GAUSS
     friend class Gaussian;
     
     template <class T>

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index cf711e4439e5727ac8583d48495de4fea9872f20..73a86c3189cc5361321f9ec3f306404d6e7df79b 100644 (file)
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -55,9 +55,8 @@ void Subsumer::extendModel(Solver& solver2)
     vec<Lit> tmp;
     typedef map<Var, vector<vector<Lit> > > elimType;
     for (elimType::iterator it = elimedOutVar.begin(), end = elimedOutVar.end(); it != end; it++) {
-        Var var = it->first;
-        
         #ifdef VERBOSE_DEBUG
+        Var var = it->first;
         std::cout << "Reinserting elimed var: " << var+1 << std::endl;
         #endif
         
@@ -793,7 +792,7 @@ const bool Subsumer::simplifyBySubsumption()
     numVarsElimed = 0;
     blockTime = 0.0;
     
-    //if (solver.clauses.size() < 2000000) addAllXorAsNorm();
+    //if (solver.xorclauses.size() < 30000 && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/10) addAllXorAsNorm();
     
     //For VE
     touched_list.clear();
@@ -933,7 +932,6 @@ const bool Subsumer::simplifyBySubsumption()
         
         for (bool first = true; numMaxElim > 0; first = false){
             uint32_t vars_elimed = 0;
-            int clauses_before = solver.nClauses();
             vec<Var> order;
             
             if (first) {
@@ -978,7 +976,7 @@ const bool Subsumer::simplifyBySubsumption()
             
             numVarsElimed += vars_elimed;
             #ifdef BIT_MORE_VERBOSITY
-            printf("c  #clauses-removed: %-8d #var-elim: %d\n", clauses_before - solver.nClauses(), vars_elimed);
+            printf("c  #var-elim: %d\n", vars_elimed);
             std::cout << "c time until the end of varelim: " << cpuTime() - myTime << std::endl;
             #endif
         }
@@ -1012,10 +1010,10 @@ const bool Subsumer::simplifyBySubsumption()
     
     addBackToSolver();
     solver.nbCompensateSubsumer += origNLearnts-solver.learnts.size();
-    /*if (solver.findNormalXors && solver.clauses.size() < MAX_CLAUSENUM_XORFIND) {
+    if (solver.findNormalXors && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/8) {
         XorFinder xorFinder(&solver, solver.clauses, ClauseCleaner::clauses);
-        if (!xorFinder.doNoPart(3, 4)) return false;
-    }*/
+        if (!xorFinder.doNoPart(3, 7)) return false;
+    }
     
     if (solver.verbosity >= 1) {
         std::cout << "c |  lits-rem: " << std::setw(9) << literals_removed
@@ -1322,7 +1320,7 @@ void Subsumer::orderVarsForElim(vec<Var>& order)
 {
     order.clear();
     vec<pair<int, Var> > cost_var;
-    for (int i = 0; i < touched_list.size(); i++){
+    for (uint32_t i = 0; i < touched_list.size(); i++){
         Var x = touched_list[i];
         touched[x] = 0;
         cost_var.push(std::make_pair( occur[Lit(x, false).toInt()].size() * occur[Lit(x, true).toInt()].size() , x ));
@@ -1331,7 +1329,7 @@ void Subsumer::orderVarsForElim(vec<Var>& order)
     touched_list.clear();
     std::sort(cost_var.getData(), cost_var.getData()+cost_var.size(), myComp());
     
-    for (int x = 0; x < cost_var.size(); x++) {
+    for (uint32_t x = 0; x < cost_var.size(); x++) {
         if (cost_var[x].first != 0)
             order.push(cost_var[x].second);
     }
@@ -1709,7 +1707,9 @@ void Subsumer::addAllXorAsNorm()
         solver.removeClause(**i);
     }
     solver.xorclauses.shrink(i-j);
-    std::cout << "Added XOR as norm:" << added << std::endl;
+    if (solver.verbosity >= 1) {
+        std::cout << "c |  Added XOR as norm:" << added << std::endl;
+    }
 }
 
 void Subsumer::addXorAsNormal3(XorClause& c)

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 43593b7fadee6817103860f3261779da5b5a864e..c9c4944b85d4e345fc24413af9838efe9c1296ff 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: fb8c4dc98c93f0034e20ce4b068457215a4047e8
+GIT revision: 9653102935b2e707c0aae731704e28809c4b548d

diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 261288ec8cfe983ee4d92e55c65012c6472f4a31..580b27ae9f0b7a0a8549a6fb696f2b3ad0c42ad4 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -152,7 +152,7 @@ const bool VarReplacer::replace_set(vec<XorClause*>& cs)
         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++) {
+        for (Lit *l = &c[0], *end2 = l + c.size(); l != end2; l++) {
             Lit newlit = table[l->var()];
             if (newlit.var() != l->var()) {
                 changed = true;
@@ -242,7 +242,7 @@ const bool VarReplacer::replace_set(vec<Clause*>& cs)
         bool changed = false;
         Lit origLit1 = c[0];
         Lit origLit2 = c[1];
-        for (Lit *l = c.getData(), *end = l + c.size();  l != end; l++) {
+        for (Lit *l = c.getData(), *end2 = l + c.size();  l != end2; l++) {
             if (table[l->var()].var() != l->var()) {
                 changed = true;
                 *l = table[l->var()] ^ l->sign();

diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h
index a223c7c0f90eae6cc9cc62613f3b52ec85fcda38..4c94beb6737457e7f3a1ffc1d5fd1c97d0ba27dd 100644 (file)
--- a/src/sat/cryptominisat2/constants.h
+++ b/src/sat/cryptominisat2/constants.h
@@ -33,3 +33,4 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define RESTART_TYPE_DECIDER_UNTIL 7
 //#define VERBOSE_DEBUG_XOR
 //#define VERBOSE_DEBUG
+//#define USE_GAUSS