Added missing functions for backtracking

src/sat/sat_config.cpp

@@ -266,6 +266,8 @@ namespace sat {
         m_xor_gauss_max_num_matrices = p.xor_gauss_max_num_matrices();
         m_xor_gauss_force_use_all_matrices = p.xor_gauss_force_use_all_matrices();
         m_xor_gauss_min_usefulness_cutoff = p.xor_gauss_min_usefulness_cutoff();
+        m_xor_gauss_autodisable = p.xor_gauss_autodisable();
+        m_xor_gauss_detach_reattach = p.xor_gauss_detach_reattach();
         
         sat_simplifier_params ssp(_p);
         m_elim_vars = ssp.elim_vars();

src/sat/sat_config.h

@@ -209,6 +209,8 @@ namespace sat {
         unsigned           m_xor_gauss_max_num_matrices;
         bool               m_xor_gauss_force_use_all_matrices;
         double             m_xor_gauss_min_usefulness_cutoff;
+        bool               m_xor_gauss_autodisable;
+        bool               m_xor_gauss_detach_reattach;
         
         const bool         m_xor_gauss_doMatrixFind = true;
         const unsigned     m_xor_gauss_min_clauses = 2;

src/sat/sat_params.pyg

@@ -133,15 +133,15 @@ def_module_params('sat',
                           # ('xor.max_to_find_slow', UINT, 'tbd'),
                           # ('xor.max_xor_matrix, UINT64, 'tbd'),
                           # ('xor.allow_elim_vars', BOOL, 'tbd'),
-                          # ('xor.var_per_cut', UINT, 'tbd'),
                           # ('xor.force_preserve_xors', BOOL, 'tbd'),
                           ('xor.gauss.max_matrix_columns', UINT, 1000, 'tbd'),
                           ('xor.gauss.max_matrix_rows', UINT,  2000, 'The maximum matrix size -- no. of rows'),
                           ('xor.gauss.min_matrix_rows', UINT,  3, 'The minimum matrix size -- no. of rows'),
                           ('xor.gauss.max_num_matrices', UINT,  5, 'Maximum number of matrices'),
-                          ('xor.gauss.force_use_all_matrices', BOOL, True, 'tbd'),
+                          ('xor.gauss.force_use_all_matrices', BOOL, False, 'Force using all matrices'),
-                          # ('xor.gauss.autodisable', BOOL, False, 'tbd'),
+                          ('xor.gauss.autodisable', BOOL, True, 'Automatically disable gauss when performing badly'),
-                          ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0.2, 'tbd'),
+                          ('xor.gauss.detach_reattach', BOOL, False, 'Detach and reattach XORs'),
+                          ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0.2, 'Turn off Gauss if less than this many usefulenss ratio is recorded'),
                           # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'),
                           # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'),
                           # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd')

src/sat/smt/xor_gaussian.cpp

@@ -162,14 +162,14 @@ EGaussian::EGaussian(xr::solver& _solver, unsigned _matrix_no, const vector<xor_
 
 EGaussian::~EGaussian() {
     delete_gauss_watch_this_matrix();
-    for (auto& x: tofree) 
+    for (auto& x: m_tofree) 
         memory::deallocate(x);
-    tofree.clear();
+    m_tofree.clear();
 
-    delete cols_unset;
+    delete m_cols_unset;
-    delete cols_vals;
+    delete m_cols_vals;
-    delete tmp_col;
+    delete m_tmp_col;
-    delete tmp_col2;
+    delete m_tmp_col2;
 }
 
 struct ColSorter {
@@ -333,23 +333,23 @@ bool EGaussian::full_init(bool& created) {
     xor_reasons.resize(m_num_rows);
     unsigned num_64b = m_num_cols / 64 + (bool)(m_num_cols % 64);
     
-    for (auto& x: tofree) 
+    for (auto& x: m_tofree) 
         memory::deallocate(x);
     
-    tofree.clear();
+    m_tofree.clear();
 
     auto add_packed_row = [&](PackedRow*& p) {
         int64_t* x = (int64_t*)memory::allocate(sizeof(int64_t) * (num_64b + 1));
-        tofree.push_back(x);
+        m_tofree.push_back(x);
         dealloc(p);
         p = alloc(PackedRow, num_64b, x);
         p->rhs() = 0;
     };
 
-    add_packed_row(cols_unset);
+    add_packed_row(m_cols_unset);
-    add_packed_row(cols_vals);
+    add_packed_row(m_cols_vals);
-    add_packed_row(tmp_col);
+    add_packed_row(m_tmp_col);
-    add_packed_row(tmp_col2);
+    add_packed_row(m_tmp_col2);
 
     initialized = true;
     update_cols_vals_set(true);
@@ -446,8 +446,8 @@ literal_vector& EGaussian::get_reason(unsigned row, int& out_ID) {
     m_mat[row].get_reason(
         to_fill,
         m_column_to_var,
-        *cols_vals,
+        *m_cols_vals,
-        *tmp_col2,
+        *m_tmp_col2,
         xor_reasons[row].m_propagated);
     
     xor_reasons[row].m_must_recalc = false;
@@ -638,10 +638,10 @@ bool EGaussian::find_truths(
         m_column_to_var,
         var_has_resp_row,
         new_resp_var,
-        *tmp_col,
+        *m_tmp_col,
-        *tmp_col2,
+        *m_tmp_col2,
-        *cols_vals,
+        *m_cols_vals,
-        *cols_unset,
+        *m_cols_unset,
         ret_lit_prop);
     find_truth_called_propgause++;
 
@@ -754,28 +754,30 @@ bool EGaussian::find_truths(
 }
 
 inline void EGaussian::update_cols_vals_set(literal lit) {
-    cols_unset->clearBit(m_var_to_column[lit.var()]);
+    m_cols_unset->clearBit(m_var_to_column[lit.var()]);
     if (!lit.sign())
-        cols_vals->setBit(m_var_to_column[lit.var()]);
+        m_cols_vals->setBit(m_var_to_column[lit.var()]);
 }
 
+// Updates the auxiliary row that determines which variables of the matrix are unassigned and which values they have
+// In case the argument is false it only updates the recently added variables. If true, it recalculates all
 void EGaussian::update_cols_vals_set(bool force) {
     SASSERT(initialized);
 
-    if (cancelled_since_val_update || force) {
+    if (recalculate_values || force) {
-        cols_vals->setZero();
+        m_cols_vals->setZero();
-        cols_unset->setOne();
+        m_cols_unset->setOne();
 
         for (unsigned col = 0; col < m_column_to_var.size(); col++) {
             unsigned var = m_column_to_var[col];
             if (m_solver.s().value(var) != l_undef) {
-                cols_unset->clearBit(col);
+                m_cols_unset->clearBit(col);
                 if (m_solver.s().value(var) == l_true)
-                    cols_vals->setBit(col);
+                    m_cols_vals->setBit(col);
             }
         }
         last_val_update = m_solver.s().trail_size();
-        cancelled_since_val_update = false;
+        recalculate_values = false;
         TRACE("xor", tout << "last val update set to " << last_val_update << "\n");         
         return;
     }
@@ -789,21 +791,21 @@ void EGaussian::update_cols_vals_set(bool force) {
         unsigned col = m_var_to_column[var];
         if (col != UINT32_MAX) {
             SASSERT(m_solver.s().value(var) != l_undef);
-            cols_unset->clearBit(col);
+            m_cols_unset->clearBit(col);
             if (m_solver.s().value(var) == l_true)
-                cols_vals->setBit(col);
+                m_cols_vals->setBit(col);
         }
     }
     last_val_update = m_solver.s().trail_size();
 
     std::cout << "Col-Unassigned: ";
-    for (int i = 0; i < 64 * cols_unset->size; ++i) {
+    for (int i = 0; i < 64 * m_cols_unset->size; ++i) {
-        std::cout << (*cols_unset)[i];
+        std::cout << (*m_cols_unset)[i];
     }
     std::cout << "\n";
     std::cout << "Col-Values:     ";
-    for (int i = 0; i < 64 * cols_vals->size; ++i) {
+    for (int i = 0; i < 64 * m_cols_vals->size; ++i) {
-        std::cout << (*cols_vals)[i];
+        std::cout << (*m_cols_vals)[i];
     }
     std::cout << std::endl;
 }
@@ -873,10 +875,10 @@ void EGaussian::eliminate_column(unsigned p, gauss_data& gqd) {
                     m_column_to_var,
                     var_has_resp_row,
                     new_non_resp_var,
-                    *tmp_col,
+                    *m_tmp_col,
-                    *tmp_col2,
+                    *m_tmp_col2,
-                    *cols_vals,
+                    *m_cols_vals,
-                    *cols_unset,
+                    *m_cols_unset,
                     ret_lit_prop
                 );
                 elim_called_propgause++;
@@ -1082,6 +1084,7 @@ bool EGaussian::check_row_satisfied(unsigned row) {
     return !fin;
 }
 
+// determines if the current matrix must be disabled because it performs badly
 bool EGaussian::must_disable(gauss_data& gqd) {
     SASSERT(initialized);
     gqd.disable_checks++;

src/sat/smt/xor_gaussian.h

@@ -585,7 +585,7 @@ namespace xr {
             unsigned p,
             gauss_data& gqd
         );
-        void canceling();
+        void enforce_recalculate();
         bool full_init(bool& created);
         void update_cols_vals_set(bool force);
         bool must_disable(gauss_data& gqd);
@@ -668,7 +668,7 @@ namespace xr {
         ///////////////
         unsigned matrix_no;
         bool initialized = false;
-        bool cancelled_since_val_update = true;
+        bool recalculate_values = true;
         unsigned last_val_update = 0;
 
         vector<xor_clause> m_xorclauses;
@@ -699,20 +699,22 @@ namespace xr {
         unsigned m_num_cols = 0;
     
         //quick lookup
-        PackedRow* cols_vals = nullptr; // the current model for the variable in the respective column. Only correct if the respective element in cols_unset is 0 (lazily -> update_cols_vals_set)
+        PackedRow* m_cols_vals = nullptr; // the current model for the variable in the respective column. Only correct if the respective element in cols_unset is 0 (lazily -> update_cols_vals_set)
-        PackedRow* cols_unset = nullptr; // initially a sequence of 1. If the variable at the respective colum in the matrix is assigned it is set to 0 (lazily -> update_cols_vals_set) 
+        PackedRow* m_cols_unset = nullptr; // initially a sequence of 1. If the variable at the respective colum in the matrix is assigned it is set to 0 (lazily -> update_cols_vals_set) 
-        PackedRow* tmp_col = nullptr;
+        PackedRow* m_tmp_col = nullptr;
-        PackedRow* tmp_col2 = nullptr;
+        PackedRow* m_tmp_col2 = nullptr;
         
         void update_cols_vals_set(literal lit);
     
         //Data to free (with delete[] x)
         // TODO: This are always 4 equally sized elements; merge them into one block  
-        svector<int64_t*> tofree;
+        svector<int64_t*> m_tofree;
     };
     
-    inline void EGaussian::canceling() {
+    // enforces to recalculate the auxiliary rows that determine which variables of the matrix are unassigned/assigned to true
-        cancelled_since_val_update = true;
+    // necessary after backtracking
+    inline void EGaussian::enforce_recalculate() {
+        recalculate_values = true;
         memset(satisfied_xors.data(), false, satisfied_xors.size());
     }
 

src/sat/smt/xor_solver.cpp

@@ -281,6 +281,12 @@ namespace xr {
         m_justifications_lim.shrink(old_sz);
         m_justifications.shrink(old_sz);*/
 
+        for (unsigned i = 0; i < m_gmatrices.size(); i++)
+            if (m_gmatrices[i] && !m_gqueuedata[i].disabled)
+                m_gmatrices[i]->enforce_recalculate();
+        
+        check_need_gauss_jordan_disable();
+        
         if (m_region)
             m_region->pop_scope(num_scopes);
     }
@@ -297,6 +303,17 @@ namespace xr {
             pop_core(n);
     }
     
+     bool solver::check_model(sat::model const& m) const {
+        for (const auto& clause : m_xorclauses) {
+            bool eval = false;
+            for (bool_var v : clause)
+                eval ^= m[v];
+            if (eval != clause.m_rhs)
+                return false;
+        }
+        return true;
+    }
+
     // inprocessing
     // pre_simplify: decompile all xor constraints to allow other in-processing.
     // simplify: recompile clauses to xor constraints
@@ -391,6 +408,25 @@ namespace xr {
         }
     }
     
+    // disables matrixes if applicable
+    void solver::check_need_gauss_jordan_disable() {
+        for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
+            auto& gqd = m_gqueuedata[i];
+            if (gqd.disabled)
+                continue;
+    
+            // TODO: Without having the xors also as clauses, this is unsound
+            /*if (s().get_config().m_xor_gauss_autodisable &&
+                !s().get_config().m_xor_gauss_detach_reattach &&
+                m_gmatrices[i]->must_disable(gqd)) {
+                gqd.disabled = true;
+            }*/
+    
+            gqd.reset();
+            m_gmatrices[i]->update_cols_vals_set(false);
+        }
+    }
+
     // throw away all assigned clash-variables and simplify xor-clause with respect to current assignment
     // may add conflict or propagate
     bool solver::clean_one_xor(xor_clause& x) {
@@ -461,7 +497,7 @@ namespace xr {
         bool ret_no_irred_nonxor_contains_clash_vars;
         if (can_detach &&
             s().get_config().m_xor_gauss_detach_reattach &&
-            !s().get_config().autodisable &&
+            !s().get_config().m_xor_gauss_autodisable &&
             (ret_no_irred_nonxor_contains_clash_vars = no_irred_nonxor_contains_clash_vars())) {
             detach_xor_clauses(mfinder.clash_vars_unused);
             unset_clash_decision_vars(xorclauses);

src/sat/smt/xor_solver.h

@@ -88,6 +88,8 @@ namespace xr {
         
         bool add_simple_xor_constraint(const xor_clause& constraint);
         
+        void check_need_gauss_jordan_disable();
+        
         bool inconsistent() const { return s().inconsistent(); }
 
     public:
@@ -136,5 +138,7 @@ namespace xr {
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
+        
+        bool check_model(sat::model const& m) const override;
 };
 }