From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 4 Dec 2009 10:36:39 +0000 (+0000)
Subject: Updating to cryptominisat2 git revision 63f0b6f7e4927759643c97913060c37f8ae4c82a
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8bca72333d94dd059a3a451af3da116e05b18a18;p=francis%2Fstp.git

Updating to cryptominisat2 git revision 63f0b6f7e4927759643c97913060c37f8ae4c82a

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

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index b1e5fc5..27f019b 100644
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -200,9 +200,6 @@ bool Conglomerate::dealWithNewClause(vec<Lit>& ps, const bool inverted, const ui
             if (S->assigns[ps[0].var()] == l_Undef) {
                 assert(S->decisionLevel() == 0);
                 S->uncheckedEnqueue(Lit(ps[0].var(), inverted));
-                ps[0] = Lit(ps[0].var(), inverted);
-                Clause* newC = Clause_new(ps, old_group);
-                S->unitary_learnts.push(newC);
             } else if (S->assigns[ps[0].var()] != boolToLBool(!inverted)) {
                 #ifdef VERBOSE_DEBUG
                 cout << "Conflict. Aborting.";
diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp
index 7630e44..3e82b8e 100644
--- a/src/sat/cryptominisat2/Gaussian.cpp
+++ b/src/sat/cryptominisat2/Gaussian.cpp
@@ -59,7 +59,8 @@ Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _m
 
 Gaussian::~Gaussian()
 {
-    clear_clauses();
+    for (uint i = 0; i < clauses_toclear.size(); i++)
+        free(clauses_toclear[i].first);
 }
 
 inline void Gaussian::set_matrixset_to_cur()
@@ -73,12 +74,6 @@ inline void Gaussian::set_matrixset_to_cur()
         matrix_sets[level] = cur_matrixset;
 }
 
-void Gaussian::clear_clauses()
-{
-    std::for_each(matrix_clauses_toclear.begin(), matrix_clauses_toclear.end(), std::ptr_fun(free));
-    matrix_clauses_toclear.clear();
-}
-
 llbool Gaussian::full_init()
 {
     if (!should_init()) return l_Nothing;
@@ -448,13 +443,13 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
             continue;
         }
 
-        uint best_row = i;
         PackedMatrix::iterator this_matrix_row = m.matrix.begin() + i;
         PackedMatrix::iterator end = m.matrix.begin() + std::min(m.last_one_in_col[j], m.num_rows);
-        for (; this_matrix_row != end; ++this_matrix_row, best_row++) {
+        for (; this_matrix_row != end; ++this_matrix_row) {
             if ((*this_matrix_row)[j])
                 break;
         }
+        uint best_row = this_matrix_row - m.matrix.begin();
 
         if (this_matrix_row != end) {
             PackedRow matrix_row_i = m.matrix[i];
@@ -655,6 +650,9 @@ void Gaussian::cancel_until_sublevel(const uint sublevel)
     #ifdef VERBOSE_DEBUG
     cout << "(" << matrix_no << ")Canceling until sublevel " << sublevel << endl;
     #endif
+    
+    for (Gaussian **gauss = &(solver.gauss_matrixes[0]), **end= gauss + solver.gauss_matrixes.size(); gauss != end; gauss++)
+        if (*gauss != this) (*gauss)->canceling(sublevel);
 
     for (int level = solver.trail.size()-1; level >= sublevel; level--) {
         Var     var  = solver.trail[level].var();
@@ -664,8 +662,6 @@ void Gaussian::cancel_until_sublevel(const uint sublevel)
 
         solver.assigns[var] = l_Undef;
         solver.insertVarOrder(var);
-        for (Gaussian **gauss = &(solver.gauss_matrixes[0]), **end= gauss + solver.gauss_matrixes.size(); gauss != end; gauss++)
-            if (*gauss != this) (*gauss)->canceling(level, var);
     }
     solver.trail.shrink(solver.trail.size() - sublevel);
     
@@ -769,13 +765,13 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row
         
         solver.cancelUntil(0);
         solver.uncheckedEnqueue(lit);
-        solver.unitary_learnts.push(&cla);
         if (solver.dynamic_behaviour_analysis)
             solver.logger.propagation(cla[0], Logger::gauss_propagation_type, cla.group);
+        free(&cla);
         return unit_propagation;
     }
 
-    matrix_clauses_toclear.push_back(&cla);
+    clauses_toclear.push_back(std::make_pair(&cla, solver.trail.size()-1));
     solver.uncheckedEnqueue(cla[0], &cla);
     if (solver.dynamic_behaviour_analysis) {
         solver.logger.set_group_name(cla.group, "gauss prop clause");
diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h
index 4730adf..1d692e7 100644
--- a/src/sat/cryptominisat2/Gaussian.h
+++ b/src/sat/cryptominisat2/Gaussian.h
@@ -60,9 +60,7 @@ public:
     void set_disabled(const bool toset);
 
     //functions used throughout the Solver
-    void back_to_level(const uint level);
-    void canceling(const uint level, const Var var);
-    void clear_clauses();
+    void canceling(const int sublevel);
 
 protected:
     Solver& solver;
@@ -101,7 +99,7 @@ protected:
     //Varibales to keep Gauss state
     bool messed_matrix_vars_since_reversal;
     int gauss_last_level;
-    vector<Clause*> matrix_clauses_toclear;
+    vector<pair<Clause*, uint> > clauses_toclear;
     bool disabled; // Gauss is disabled
     
     //State of current elimnation
@@ -173,15 +171,29 @@ inline bool Gaussian::should_check_gauss(const uint decisionlevel, const uint st
             && decisionlevel < config.decision_until);
 }
 
-inline void Gaussian::canceling(const uint level, const Var var)
+inline void Gaussian::canceling(const int sublevel)
 {
-    if (!messed_matrix_vars_since_reversal
-            && level <= gauss_last_level
-            && var < var_is_in.getSize()
+    if (disabled)
+        return;
+    uint a = 0;
+    for (int i = clauses_toclear.size()-1; i >= 0 && clauses_toclear[i].second > sublevel; i--) {
+        free(clauses_toclear[i].first);
+        a++;
+    }
+    clauses_toclear.resize(clauses_toclear.size()-a);
+    
+    if (messed_matrix_vars_since_reversal)
+        return;
+    int c = std::min(gauss_last_level, solver.trail.size()-1);
+    for (; c >= sublevel; c--) {
+        Var var  = solver.trail[c].var();
+        if (var < var_is_in.getSize()
             && var_is_in[var]
-            && cur_matrixset.var_is_set[var]
-       )
+            && cur_matrixset.var_is_set[var]) {
         messed_matrix_vars_since_reversal = true;
+        return;
+        }
+    }
 }
 
 inline void Gaussian::print_matrix_stats() const
diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp
index d70ca14..a89b9f9 100644
--- a/src/sat/cryptominisat2/Logger.cpp
+++ b/src/sat/cryptominisat2/Logger.cpp
@@ -166,6 +166,7 @@ void Logger::first_begin()
 
 void Logger::begin()
 {
+    begin_called = true;
     if (proof_graph_on) {
         std::stringstream filename;
         filename << "proofs/" << runid << "-proof" << S->starts << ".dot";
@@ -628,7 +629,7 @@ void Logger::print_learnt_clause_distrib() const
             it->second++;
     }
     
-    learnt_sizes[0] = S->get_unitary_learnts().size();
+    learnt_sizes[0] = S->get_unitary_learnts_num();
     
     uint slice = (maximum+1)/max_print_lines + (bool)((maximum+1)%max_print_lines);
     
@@ -719,7 +720,7 @@ void Logger::print_general_stats() const
     print_line("Number of literals in clauses",S->clauses_literals);
     print_line("Avg. literals per learnt clause",(double)S->learnts_literals/(double)S->nLearnts());
     print_line("Progress estimate (%):", S->progress_estimate*100.0);
-    print_line("All unitary learnts until now", S->unitary_learnts.size());
+    print_line("All unitary learnts until now", S->get_unitary_learnts_num());
     
     print_footer();
 }
diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp
index def2113..d3847db 100644
--- a/src/sat/cryptominisat2/MatrixFinder.cpp
+++ b/src/sat/cryptominisat2/MatrixFinder.cpp
@@ -78,6 +78,9 @@ const uint MatrixFinder::findMatrixes()
     if (S->xorclauses.size() == 0)
         return 0;
     
+    S->removeSatisfied(S->xorclauses);
+    S->cleanClauses(S->xorclauses);
+    
     for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) {
         set<uint> tomerge;
         vector<Var> newSet;
diff --git a/src/sat/cryptominisat2/PackedMatrix.h b/src/sat/cryptominisat2/PackedMatrix.h
index 602f54e..854f30b 100644
--- a/src/sat/cryptominisat2/PackedMatrix.h
+++ b/src/sat/cryptominisat2/PackedMatrix.h
@@ -134,6 +134,11 @@ public:
             return ret;
         }
         
+        const uint operator-(const iterator& b) const
+        {
+            return (mp - b.mp)/(numCols+1);
+        }
+        
         void operator+=(const uint num)
         {
             mp += (numCols+1)*num;
diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h
index 2184ae4..01fa26e 100644
--- a/src/sat/cryptominisat2/PackedRow.h
+++ b/src/sat/cryptominisat2/PackedRow.h
@@ -94,9 +94,11 @@ public:
         assert(b.size == size);
         #endif
         
-        memcpy(tmp_row, b.mp-1, sizeof(uint64_t)*(size+1));
-        memcpy(b.mp-1, mp-1, sizeof(uint64_t)*(size+1));
-        memcpy(mp-1, tmp_row, sizeof(uint64_t)*(size+1));
+        for (int i = -1; i != size; i++) {
+            uint64_t tmp(*(b.mp + i));
+            *(b.mp + i) = *(mp + i);
+            *(mp + i) = tmp;
+        }
     }
 
     PackedRow& operator^=(const PackedRow& b);
diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index c5abee0..46f7062 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -37,7 +37,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Conglomerate.h"
 #include "XorFinder.h"
 
-//#define DEBUG_LIB
+#define DEBUG_LIB
 
 #ifdef DEBUG_LIB
 #include <sstream>
@@ -111,11 +111,10 @@ Solver::Solver() :
 Solver::~Solver()
 {
     for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
-    for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_learnts[i]);
     for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
     for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]);
     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]);
     delete toReplace;
     delete conglomerate;
     
@@ -177,7 +176,8 @@ bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint gro
     Lit p;
     int i, j;
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
-        ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+        if (toReplace->getNumReplacedLits())
+            ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         xor_clause_inverted ^= ps[i].sign();
         ps[i] ^= ps[i].sign();
 
@@ -252,7 +252,8 @@ bool Solver::addClause(vec<Lit>& ps, const uint group, char* group_name)
     Lit p;
     int i, j;
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
-        ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+        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)
@@ -396,13 +397,15 @@ void Solver::cancelUntil(int level)
     #endif
     
     if (decisionLevel() > level) {
+        
+        for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
+            (*gauss)->canceling(trail_lim[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;
             #endif
-            for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
-                (*gauss)->canceling(c, x);
             assigns[x] = l_Undef;
             insertVarOrder(x);
         }
@@ -1021,9 +1024,15 @@ const vec<Clause*>& Solver::get_sorted_learnts()
     return learnts;
 }
 
-const vec<Clause*>& Solver::get_unitary_learnts() const
+const vector<Lit> Solver::get_unitary_learnts() const
 {
-    return unitary_learnts;
+    vector<Lit> unitaries;
+    if (decisionLevel() > 0) {
+        for (uint i = 0; i < trail_lim[0]; i++)
+            unitaries.push_back(trail[i]);
+    }
+    
+    return unitaries;
 }
 
 void Solver::dump_sorted_learnts(const char* file)
@@ -1034,8 +1043,10 @@ void Solver::dump_sorted_learnts(const char* file)
         exit(-1);
     }
     
-    for (uint i = 0; i < unitary_learnts.size(); i++)
-        unitary_learnts[i]->plain_print(outfile);
+    if (decisionLevel() > 0) {
+        for (uint i = 0; i < trail_lim[0]; i++)
+            printf("%s%d 0\n", trail[i].sign() ? "-" : "", trail[i].var());
+    }
     
     sort(learnts, reduceDB_lt());
     for (int i = learnts.size()-1; i >= 0 ; i--) {
@@ -1203,8 +1214,6 @@ lbool Solver::search(int nof_conflicts)
         if (ret != l_Nothing) return ret;
     }
 
-    if (dynamic_behaviour_analysis) logger.begin();
-
     for (;;) {
         Clause* confl = propagate();
 
@@ -1334,12 +1343,11 @@ llbool Solver::handle_conflict(vec<Lit>& learnt_clause, Clause* confl, int& conf
     assert(value(learnt_clause[0]) == l_Undef);
     //Unitary learnt
     if (learnt_clause.size() == 1) {
-        Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true);
-        unitary_learnts.push(c);
         uncheckedEnqueue(learnt_clause[0]);
         if (dynamic_behaviour_analysis) {
-            logger.set_group_name(c->group, "unitary learnt clause");
-            logger.propagation(learnt_clause[0], Logger::unit_clause_type, c->group);
+            logger.set_group_name(learnt_clause_group, "unitary learnt clause");
+            logger.propagation(learnt_clause[0], Logger::unit_clause_type, learnt_clause_group);
+            learnt_clause_group++;
         }
         assert(backtrack_level == 0 && "Unit clause learnt, so must cancel until level 0, right?");
         
@@ -1415,9 +1423,6 @@ lbool Solver::solve(const vec<Lit>& assumps)
     fprintf(myoutputfile, "c Solver::solve() called\n");
     #endif
     
-    if (dynamic_behaviour_analysis)
-        logger.end(Logger::done_adding_clauses);
-    
     model.clear();
     conflict.clear();
 
@@ -1492,9 +1497,14 @@ 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 (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) {
-        removeSatisfied(xorclauses);
-        cleanClauses(xorclauses);
         double time = cpuTime();
         MatrixFinder m(this);
         const uint numMatrixes = m.findMatrixes();
@@ -1509,6 +1519,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
         printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl | Prop   Confl   On  |\n");
         printf("=========================================================================================\n");
     }
+    
+    if (dynamic_behaviour_analysis)
+        logger.end(Logger::done_adding_clauses);
 
     // Search:
     while (status == l_Undef && starts < maxRestarts) {
@@ -1527,11 +1540,10 @@ lbool Solver::solve(const vec<Lit>& assumps)
         for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
             (*gauss)->reset_stats();
         
+        if (dynamic_behaviour_analysis)
+            logger.begin();
         status = search((int)nof_conflicts);
         nof_conflicts *= restart_inc;
-        
-        for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
-            (*gauss)->clear_clauses();
     }
 
     if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 45e3f83..2769809 100644
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -157,7 +157,8 @@ public:
     void setVariableName(int var, char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger')
     const vec<Clause*>& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses
     const vec<Clause*>& get_learnts() const; //Get all learnt clauses
-    const vec<Clause*>& get_unitary_learnts() const; //return the set of unitary learned clauses
+    const vector<Lit> get_unitary_learnts() const; //return the set of unitary learnt clauses
+    const uint get_unitary_learnts_num() const; //return the number of unitary learnt clauses
     void dump_sorted_learnts(const char* file);
 
 protected:
@@ -192,7 +193,7 @@ protected:
     vec<Clause*>        clauses;          // List of problem clauses.
     vec<XorClause*>     xorclauses;       // List of problem xor-clauses. Will be freed
     vec<Clause*>        learnts;          // List of learnt clauses.
-    vec<Clause*>        unitary_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<Clause*> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
@@ -434,6 +435,12 @@ inline void     Solver::needRealUnknowns()
 {
     useRealUnknowns = true;
 }
+inline const uint Solver::get_unitary_learnts_num() const
+{
+    if (decisionLevel() > 0)
+        return trail_lim[0];
+    return 0;
+}
 template<class T>
 void Solver::removeSatisfied(vec<T*>& cs)
 {
@@ -491,6 +498,7 @@ inline void Solver::removeClause(Clause& c)
 inline void Solver::removeClause(XorClause& c)
 {
     detachClause(c);
+    freeLater.push(&c);
     c.mark(1);
 }
 
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 0814fa6..8ac9e02 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,4 +1,4 @@
 CryptoMiniSat
-SVN revision: 519
-GIT revision: 0426e61b02a00a073a87fdffc0282820875fad61
+SVN revision: 
+GIT revision: 63f0b6f7e4927759643c97913060c37f8ae4c82a
 
diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 4e08cd1..d6cfb3b 100644
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -58,7 +58,6 @@ void VarReplacer::performReplace()
     if (S->verbosity >=1)
         printf("|  Replacing   %8d vars, replaced %8d lits                          |\n", replacedVars, replacedLits);
     
-    replacedLits = 0;
     addedNewClause = false;
     
     if (S->ok)