Bugfix + refactoring

src/sat/smt/xor_gaussian.cpp

@@ -29,11 +29,12 @@ using namespace xr;
 static const unsigned unassigned_col = UINT32_MAX;
 
 ///returns popcnt
-unsigned PackedRow::find_watchVar(
+unsigned PackedRow::population_cnt(
-    literal_vector& tmp_clause,
+    literal_vector &tmp_clause,
     const unsigned_vector& col_to_var,
     bool_vector &var_has_resp_row,
     unsigned& non_resp_var) {
+    
     unsigned popcnt = 0;
     non_resp_var = UINT_MAX;
     tmp_clause.clear();
@@ -44,18 +45,14 @@ unsigned PackedRow::find_watchVar(
             unsigned var = col_to_var[i];
             tmp_clause.push_back(sat::literal(var, false));
 
-            if (!var_has_resp_row[var]) {
+            if (!var_has_resp_row[var])
                 non_resp_var = var;
-            } else {
+            else
-                //What??? WARNING
-                //This var already has a responsible for it...
-                //How can it be 1???
                 std::swap(tmp_clause[0], tmp_clause.back());
         }
     }
-    }
     SASSERT(tmp_clause.size() == popcnt);
-    SASSERT(popcnt == 0 || var_has_resp_row[ tmp_clause[0].var() ]) ;
+    SASSERT(popcnt == 0 || var_has_resp_row[tmp_clause[0].var()]) ;
     return popcnt;
 }
 
@@ -261,6 +258,7 @@ void EGaussian::select_columnorder() {
     }
 }
 
+// Sets up some of the required datastructures to apply initial elimination (e.g., like the matrix itself and an empty list of gaussian watchlist)
 void EGaussian::fill_matrix() {
     var_to_col.clear();
 
@@ -268,9 +266,9 @@ void EGaussian::fill_matrix() {
     select_columnorder();
     num_rows = m_xorclauses.size();
     num_cols = col_to_var.size();
-    if (num_rows == 0 || num_cols == 0) {
+    if (num_rows == 0 || num_cols == 0)
         return;
-    }
+    
     mat.resize(num_rows, num_cols); // initial gaussian matrix
 
     for (unsigned row = 0; row < num_rows; row++) {
@@ -294,12 +292,14 @@ void EGaussian::fill_matrix() {
     satisfied_xors.resize(num_rows, false);
 }
 
+// deletes all gaussian watches from the matrix for all variables
 void EGaussian::delete_gauss_watch_this_matrix() {
     for (unsigned i = 0; i < m_solver.m_gwatches.size(); i++) 
         clear_gwatches(i);    
 }
 
-void EGaussian::clear_gwatches(unsigned var) {
+// deletes all gaussian watches from the matrix for the given variable
+void EGaussian::clear_gwatches(bool_var var) {
     //if there is only one matrix, don't check, just empty it
     if (m_solver.m_gmatrices.empty()) {
         m_solver.m_gwatches[var].clear();
@@ -345,7 +345,7 @@ bool EGaussian::full_init(bool& created) {
                 return false;
             case gret::prop:
                 SASSERT(m_solver.m_num_scopes == 0);
-                m_solver.s().propagate(false); // TODO: Can we really do this here?
+                m_solver.s().propagate(false);
                 if (inconsistent()) {
                     TRACE("xor", tout << "eliminate & adjust matrix during init lead to UNSAT\n";);
                     return false;
@@ -361,7 +361,7 @@ bool EGaussian::full_init(bool& created) {
     TRACE("xor", tout << "initialised matrix " << matrix_no << "\n");
 
     xor_reasons.resize(num_rows);
-    unsigned num_64b = num_cols/64+(bool)(num_cols%64);
+    unsigned num_64b = num_cols / 64 + (bool)(num_cols % 64);
     
     for (auto& x: tofree) 
         memory::deallocate(x);
@@ -394,11 +394,11 @@ static void print_matrix(ostream& out, PackedMatrix& mat) {
         for(int i = 0; i < row.get_size() * 64; i++) {
             out << (int)row[i];
         }
-        out << " -- rhs: " << row.rhs() << " -- row:" << rowIdx << "\n";
+        out << " -- rhs: " << row.rhs() << " -- row: " << rowIdx << "\n";
     }
-    out << "\n";
 }
 
+// Applies Gaussian-Jordan elimination (search level). This function does not add conflicts/propagate/... Just reduces the matrix
 void EGaussian::eliminate() {
     // TODO: Why twice? gauss_jordan_elim
     unsigned end_row = num_rows;
@@ -406,6 +406,8 @@ void EGaussian::eliminate() {
     unsigned row_i = 0;
     unsigned col = 0;
 
+    //print_matrix(std::cout, mat);
+    //std::cout << std::endl;
     TRACE("xor", print_matrix(tout, mat));
 
     // Gauss-Jordan Elimination
@@ -441,7 +443,10 @@ void EGaussian::eliminate() {
         }
         col++;
         TRACE("xor", print_matrix(tout, mat));
+        //print_matrix(std::cout, mat);
+        //std::cout << std::endl;
     }
+    //std::cout << "-------------" << std::endl;
 }
 
 literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) {
@@ -467,6 +472,7 @@ literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) {
     return &to_fill;
 }
 
+// Creates binary clauses, assigns variables, adds conflicts based on the (reduced) gaussian-matrix. Also sets up the gaussian watchlist
 gret EGaussian::init_adjust_matrix() {
     SASSERT(m_solver.s().at_search_lvl());
     SASSERT(row_to_var_non_resp.empty());
@@ -479,7 +485,7 @@ gret EGaussian::init_adjust_matrix() {
         if (row_i >= num_rows)
             break;
         unsigned non_resp_var;
-        unsigned popcnt = row.find_watchVar(tmp_clause, col_to_var, var_has_resp_row, non_resp_var);
+        unsigned popcnt = row.population_cnt(tmp_clause, col_to_var, var_has_resp_row, non_resp_var);
 
         switch (popcnt) {
 
@@ -610,6 +616,7 @@ bool EGaussian::find_truths(
     unsigned var,
     unsigned row_n,
     gauss_data& gqd) {
+    
     SASSERT(gqd.status != gauss_res::confl);
     SASSERT(initialized);
 

src/sat/smt/xor_gaussian.h

@@ -398,7 +398,7 @@ namespace xr {
         }
     
         // using find nonbasic and basic value
-        unsigned find_watchVar(
+        unsigned population_cnt(
             sat::literal_vector& tmp_clause,
             const unsigned_vector& col_to_var,
             bool_vector &var_has_resp_row,
@@ -432,6 +432,7 @@ namespace xr {
         }
     };
     
+    // A gaussian matrix (only the very basic data)
     class PackedMatrix {
     public:
         PackedMatrix() { }
@@ -556,6 +557,7 @@ namespace xr {
         int numCols = 0;
     };
     
+    // A single gaussian matrix
     class EGaussian {
     public:
         EGaussian(
@@ -596,7 +598,7 @@ namespace xr {
         xr::solver& m_solver;   // original sat solver
     
         //Cleanup
-        void clear_gwatches(unsigned var);
+        void clear_gwatches(bool_var var);
         void delete_gauss_watch_this_matrix();
         void delete_gausswatch(unsigned row_n);
     

src/sat/smt/xor_matrix_finder.cpp

@@ -57,11 +57,9 @@ namespace xr {
     
         m_xor.move_xors_without_connecting_vars_to_unused();
         m_xor.clean_equivalent_xors(m_xor.m_xorclauses);
-        for (const auto& c : m_xor.m_xorclauses_unused){
+        for (const auto& c : m_xor.m_xorclauses_unused) 
-            for (const auto& v : c) {
+            for (const auto& v : c) 
                 clash_vars_unused.insert(v);
-            }
-        }
     
         if (m_xor.m_xorclauses.size() < m_sat.get_config().m_xor_gauss_min_clauses) {
             can_detach = false;

src/sat/smt/xor_solver.cpp

@@ -146,6 +146,8 @@ namespace xr {
     sat::justification solver::gauss_jordan_elim(const sat::literal p, const unsigned currLevel) {
         if (m_gmatrices.empty()) 
             return sat::justification(-1);
+        m_gwatches.resize(s().num_vars());
+        
         for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
             if (m_gqueuedata[i].disabled || !m_gmatrices[i]->is_initialized()) continue;
             m_gqueuedata[i].reset();
@@ -156,11 +158,11 @@ namespace xr {
         SASSERT(m_gwatches.size() > p.var());
         svector<gauss_watched>& ws = m_gwatches[p.var()];
         unsigned i = 0, j = 0;
-        const unsigned end = ws.size();
+        unsigned end = ws.size();
         
         for (; i < end; i++) {
-            const unsigned matrix_num = ws[i].matrix_num; 
+            unsigned matrix_num = ws[i].matrix_num; 
-            const unsigned row_n = ws[i].row_n; 
+            unsigned row_n = ws[i].row_n; 
             if (m_gqueuedata[matrix_num].disabled || !m_gmatrices[matrix_num]->is_initialized())
                 continue; //remove watch and continue
         
@@ -169,10 +171,7 @@ namespace xr {
             m_gqueuedata[matrix_num].do_eliminate = false;
             m_gqueuedata[matrix_num].currLevel = currLevel;
         
-            if (m_gmatrices[matrix_num]->find_truths(ws, i, j, p.var(), row_n, m_gqueuedata[matrix_num])) {
+            if (!m_gmatrices[matrix_num]->find_truths(ws, i, j, p.var(), row_n, m_gqueuedata[matrix_num])) {
-                continue;
-            } 
-            else {
                 confl_in_gauss = true;
                 i++;
                 break;
@@ -181,7 +180,7 @@ namespace xr {
         
         for (; i < end; i++) 
             ws[j++] = ws[i];
-        ws.shrink((unsigned)(i - j));
+        ws.shrink(j);
         
         for (unsigned g = 0; g < m_gqueuedata.size(); g++) {
             if (m_gqueuedata[g].disabled || !m_gmatrices[g]->is_initialized())
@@ -285,7 +284,7 @@ namespace xr {
         return out;
     }
 
-    // simplify xors by triggering (unit)propagation until nothing changes anymore
+    // simplify xors based on current assignments by triggering (unit)propagation until nothing changes anymore
     bool solver::clean_xor_clauses(vector<xor_clause>& xors) {     
         SASSERT(!inconsistent());
         
@@ -416,6 +415,8 @@ namespace xr {
         if (!m_xor_clauses_updated/* && (!m_detached_xor_clauses || !assump_contains_xor_clash())*/)
             return true;
         
+        m_gwatches.resize(s().num_vars());
+        
         bool can_detach;
         if (!clear_gauss_matrices(false)) 
             return false;
@@ -575,6 +576,8 @@ namespace xr {
         ps.shrink(j);
     }
     
+    // Creates bigger xors by gluing together xors (x1 + x2 + x3 = 0 & x3 + x4 + x5 = 0 ==> x1 + x2 + x4 + x5 = 0) and removing the glued variable
+    // This can be done if the glued variable (x3) occurs in exactly two different xor clauses and nowhere else 
     bool solver::xor_together_xors(vector<xor_clause>& xors) {
         
         if (xors.empty())
@@ -592,7 +595,7 @@ namespace xr {
         
         SASSERT(!s().inconsistent());
         SASSERT(s().at_search_lvl());
-        const size_t origsize = xors.size();
+        unsigned origsize = xors.size();
     
         SASSERT(m_occurrences.empty());
 

src/sat/smt/xor_solver.h

@@ -79,29 +79,6 @@ namespace xr {
         
         bool inconsistent() const { return s().inconsistent(); }
 
-        // TODO: CMS watches the literals directly; Z3 their negation. "_neg_" just for now to avoid confusion
-        bool is_neg_watched(sat::watch_list& l, size_t idx) const {
-            return l.contains(sat::watched((sat::ext_constraint_idx)idx));
-        }
-        
-        bool is_neg_watched(literal lit, size_t idx) const {
-            return s().get_wlist(lit).contains(sat::watched((sat::ext_constraint_idx)idx));
-        }
-        
-        void unwatch_neg_literal(literal lit, size_t idx) {
-            s().get_wlist(lit).erase(sat::watched(idx));
-            SASSERT(!is_neg_watched(lit, idx));
-        }
-        
-        void watch_neg_literal(sat::watch_list& l, size_t idx) {
-            SASSERT(!is_neg_watched(l, idx));
-            l.push_back(sat::watched(idx));
-        }
-        
-        void watch_neg_literal(literal lit, size_t idx) {
-            watch_neg_literal(s().get_wlist(lit), idx);
-        }
-
     public:
         solver(euf::solver& ctx);
         solver(ast_manager& m, euf::theory_id id);