From 8a34104101ea4c9bda235a867ac8ae85d9f95b37 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 1 Dec 2022 20:12:10 +0100 Subject: [PATCH] Refactoring --- src/sat/smt/xor_gaussian.cpp | 33 ++++++++++++++++++++++----------- src/sat/smt/xor_gaussian.h | 32 +++++++++++--------------------- 2 files changed, 33 insertions(+), 32 deletions(-) diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp index 5216d7a56..699fb9679 100644 --- a/src/sat/smt/xor_gaussian.cpp +++ b/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(); diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h index e5cd54d9b..493b7f218 100644 --- a/src/sat/smt/xor_gaussian.h +++ b/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 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 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; }