Refactoring

src/sat/smt/xor_gaussian.cpp

@@ -314,6 +314,9 @@ void EGaussian::clear_gwatches(const unsigned var) {
     m_solver.m_gwatches[var].shrink(j);
 }
 
+// Simplify matrix by applying gaussian elimination
+// This is only done at search level. We therefore can safely remove/replace "redundant" xor-clauses by unit/binary-clauses
+// Furthermore, initializes additional datastructures (e.g., for doing variable lookup)
 bool EGaussian::full_init(bool& created) {
     SASSERT(!inconsistent());
     SASSERT(m_solver.m_num_scopes == 0);
@@ -321,12 +324,12 @@ bool EGaussian::full_init(bool& created) {
     created = true;
 
     unsigned trail_before;
-    while (true) {
+    do {
         trail_before = m_solver.s().trail_size();
         m_solver.clean_xor_clauses(m_xorclauses);
 
         fill_matrix();
-        before_init_density = get_density();
+
         if (num_rows == 0 || num_cols == 0) {
             created = false;
             return !inconsistent();
@@ -351,11 +354,9 @@ bool EGaussian::full_init(bool& created) {
             default:
                 break;
         }
-        
-        //Let's exit if nothing new happened
-        if (m_solver.s().trail_size() == trail_before)
-            break;
-    }
+
+    } while (m_solver.s().trail_size() != trail_before); // Exit if nothing new happened
+
     DEBUG_CODE(check_watchlist_sanity(););
     TRACE("xor", tout << "initialised matrix " << matrix_no << "\n");
 
@@ -380,8 +381,6 @@ bool EGaussian::full_init(bool& created) {
     add_packed_row(tmp_col);
     add_packed_row(tmp_col2);
 
-    after_init_density = get_density();
-
     initialized = true;
     update_cols_vals_set(true);
     DEBUG_CODE(check_invariants(););
@@ -389,6 +388,17 @@ bool EGaussian::full_init(bool& created) {
     return !inconsistent();
 }
 
+static void print_matrix(ostream& out, PackedMatrix& mat) {
+    for (unsigned rowIdx = 0; rowIdx < mat.num_rows(); rowIdx++) {
+        const PackedRow& row = mat[rowIdx];
+        for(int i = 0; i < row.get_size() * 64; i++) {
+            out << (int)row[i];
+        }
+        out << " -- rhs: " << row.rhs() << " -- row:" << rowIdx << "\n";
+    }
+    out << "\n";
+}
+
 void EGaussian::eliminate() {
     // TODO: Why twice? gauss_jordan_elim
     const unsigned end_row = num_rows;
@@ -396,6 +406,8 @@ void EGaussian::eliminate() {
     unsigned row_i = 0;
     unsigned col = 0;
 
+    TRACE("xor", print_matrix(tout, mat));
+
     // Gauss-Jordan Elimination
     while (row_i != num_rows && col != num_cols) {
         unsigned row_with_1_in_col = rowI;
@@ -428,6 +440,7 @@ void EGaussian::eliminate() {
             ++rowI;
         }
         col++;
+        TRACE("xor", print_matrix(tout, mat));
     }
 }
 
@@ -477,7 +490,6 @@ gret EGaussian::init_adjust_matrix() {
 
                 // conflict
                 if (row.rhs()) {
-                    // TODO: Is this enough? What's the justification?
                     m_solver.s().set_conflict();
                     TRACE("xor", tout << "-> empty clause during init_adjust_matrix";);
                     TRACE("xor", tout << "-> conflict on row: " << row_i;);
@@ -763,7 +775,6 @@ inline void EGaussian::update_cols_vals_set(const literal lit1) {
 void EGaussian::update_cols_vals_set(bool force) {
     SASSERT(initialized);
 
-    //cancelled_since_val_update = true;
     if (cancelled_since_val_update || force) {
         cols_vals->setZero();
         cols_unset->setOne();

src/sat/smt/xor_gaussian.h

@@ -265,16 +265,15 @@ namespace xr {
         
         friend class PackedMatrix;
         friend class EGaussian;
-        friend std::ostream& operator<<(std::ostream& os, const PackedRow& m);
 
         PackedRow(const unsigned _size, int64_t* const _mp) :
             mp(_mp+1),
             rhs_internal(*_mp), 
             size(_size) {}
        
-           int64_t* __restrict const mp;
-           int64_t& rhs_internal;
-           const int size;
+        int64_t* __restrict const mp;
+        int64_t& rhs_internal;
+        const int size;
         
     public:
         
@@ -296,6 +295,10 @@ namespace xr {
     
             return *this;
         }
+
+        int get_size() const {
+            return size;
+        }
         
         void set_and(const PackedRow& a, const PackedRow& b) {
             for (int i = 0; i < size; i++) 
@@ -583,8 +586,6 @@ namespace xr {
         void check_watchlist_sanity();
         void move_back_xor_clauses();
     
-        vector<xor_clause> m_xorclauses;
-    
     private:
         xr::solver& m_solver;   // original sat solver
     
@@ -609,7 +610,6 @@ namespace xr {
         void fill_matrix();
         void select_columnorder();
         gret init_adjust_matrix(); // adjust matrix, include watch, check row is zero, etc.
-        double get_density();
     
         //Helper functions
         void prop_lit(const gauss_data& gqd, const unsigned row_i, const sat::literal ret_lit_prop);
@@ -632,8 +632,6 @@ namespace xr {
         unsigned elim_ret_confl = 0;
         unsigned elim_ret_satisfied = 0;
         unsigned elim_ret_fnewwatch = 0;
-        double before_init_density = 0;
-        double after_init_density = 0;
         
         ///////////////
         // Internal data
@@ -642,7 +640,9 @@ namespace xr {
         bool initialized = false;
         bool cancelled_since_val_update = true;
         unsigned last_val_update = 0;
-    
+
+        vector<xor_clause> m_xorclauses;
+
         // Is the clause at this ROW satisfied already?
         // satisfied_xors[row] tells me that
         // TODO: Maybe compress further
@@ -679,17 +679,7 @@ namespace xr {
         cancelled_since_val_update = true;
         memset(satisfied_xors.data(), false, satisfied_xors.size());
     }
-    
-    inline double EGaussian::get_density() {
-        if (num_rows*num_cols == 0)
-            return 0;
-    
-        unsigned pop = 0;
-        for (const auto& row: mat) 
-            pop += row.popcnt();        
-        return (double)pop/(double)(num_rows*num_cols);
-    }
-    
+
     inline void EGaussian::update_matrix_no(unsigned n) {
         matrix_no = n;
     }