From dc9069641c748083974725426860e21a114b91ba Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 30 Nov 2022 10:49:41 +0100 Subject: [PATCH] Changes --- src/sat/smt/xor_gaussian.cpp | 17 ++++--- src/sat/smt/xor_gaussian.h | 16 +++++-- src/sat/smt/xor_solver.cpp | 90 ++++++++++++++++++++++++------------ src/sat/smt/xor_solver.h | 25 ++++++++-- 4 files changed, 102 insertions(+), 46 deletions(-) diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp index 1af5a0f20..5216d7a56 100644 --- a/src/sat/smt/xor_gaussian.cpp +++ b/src/sat/smt/xor_gaussian.cpp @@ -816,27 +816,27 @@ bool EGaussian::inconsistent() const { void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) { const unsigned new_resp_row_n = gqd.new_resp_row; - PackedMatrix::iterator rowI = mat.begin(); - PackedMatrix::iterator end = mat.end(); const unsigned new_resp_col = var_to_col[gqd.new_resp_var]; + unsigned row_size = mat.num_rows(); unsigned row_i = 0; elim_called++; - while (rowI != end) { + while (row_i < row_size) { //Row has a '1' in eliminating column, and it's not the row responsible - if (new_resp_row_n != row_i && (*rowI)[new_resp_col]) { + PackedRow row = mat[row_i]; + if (new_resp_row_n != row_i && row[new_resp_col]) { // detect orignal non-basic watch list change or not unsigned orig_non_resp_var = row_to_var_non_resp[row_i]; unsigned orig_non_resp_col = var_to_col[orig_non_resp_var]; - SASSERT((*rowI)[orig_non_resp_col]); + SASSERT(row[orig_non_resp_col]); TRACE("xor", tout << "--> This row " << row_i << " is being watched on var: " << orig_non_resp_var + 1 << " i.e. it must contain '1' for this var's column";); SASSERT(!satisfied_xors[row_i]); - (*rowI).xor_in(*(mat.begin() + new_resp_row_n)); + row.xor_in(*(mat.begin() + new_resp_row_n)); elim_xored_rows++; @@ -844,7 +844,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) { // (it's the only '1' in that column). // But non-responsible can be eliminated. So let's check that // and then deal with it if we have to - if (!(*rowI)[orig_non_resp_col]) { + if (!row[orig_non_resp_col]) { // Delete orignal non-responsible var from watch list if (orig_non_resp_var != gqd.new_resp_var) { @@ -857,7 +857,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) { literal ret_lit_prop; unsigned new_non_resp_var = 0; - const gret ret = (*rowI).propGause( + const gret ret = row.propGause( col_to_var, var_has_resp_row, new_non_resp_var, @@ -950,7 +950,6 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) { TRACE("xor", tout << "--> OK, this row " << row_i << " still contains '1', can still be responsible";); } } - ++rowI; row_i++; } diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h index 2598a7eb6..e5cd54d9b 100644 --- a/src/sat/smt/xor_gaussian.h +++ b/src/sat/smt/xor_gaussian.h @@ -476,11 +476,11 @@ namespace xr { } inline PackedRow operator[](const unsigned i) { - return PackedRow(numCols, mp+i*(numCols+1)); + return PackedRow(numCols, mp + i * (numCols + 1)); } inline PackedRow operator[](const unsigned i) const { - return PackedRow(numCols, mp+i*(numCols+1)); + return PackedRow(numCols, mp + i * (numCols + 1)); } class iterator { @@ -497,7 +497,7 @@ namespace xr { } iterator& operator++() { - mp += (numCols+1); + mp += numCols + 1; return *this; } @@ -529,9 +529,17 @@ namespace xr { } inline iterator end() { - return iterator(mp+numRows*(numCols+1), numCols); + return iterator(mp+numRows* (numCols + 1), numCols); + } + + inline unsigned num_rows() const { + return numRows; } + inline unsigned num_cols() const { + return numCols; + } + private: int64_t* mp = nullptr; diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 08bc872f4..7c1b66477 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -71,7 +71,7 @@ namespace xr { lastlit_added = to_add; } - // TODO: Implement the following function. Unfortunately, it is needed + // TODO: Implement the following function. Unfortunately, it is needed (every xor constraint is also present as an ordinary CNF; e.g., if there is only a single xor constraint no GJ elimination will be performed) // add_xor_clause_inter_cleaned_cut(xorlits, attach); if (s().inconsistent()) break; @@ -109,12 +109,16 @@ namespace xr { if (rhs) ps[0].neg(); - add_every_combination_xor(ps, attach); + //add_every_combination_xor(ps, attach); TODO: Blasts xors; ignored for now if (ps.size() > 2) { m_xor_clauses_updated = true; m_xorclauses.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars)); m_xorclauses_orig.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars)); } + else { + // TODO: This completely ignore xors of size <= 2. The case of 2 has to be treated with more care + add_simple_xor_constraint(xor_clause(ps, rhs, m_tmp_xor_clash_vars)); + } } void solver::asserted(sat::literal l) { @@ -170,7 +174,7 @@ namespace xr { } else { confl_in_gauss = true; - i++; // TODO: That's strange, but this is really written this was in CMS + i++; break; } } @@ -280,7 +284,8 @@ namespace xr { std::ostream& solver::display(std::ostream& out) const { return out; } - + + // simplify xors by triggering (unit)propagation until nothing changes anymore bool solver::clean_xor_clauses(vector& xors) { SASSERT(!inconsistent()); @@ -313,7 +318,51 @@ namespace xr { return !inconsistent(); } + // Adds xor constraints of size 0, 1 and 2. In case the constraint is larger the function returns true + bool solver::add_simple_xor_constraint(const xor_clause& constraint) { + SASSERT(!inconsistent()); + switch (constraint.size()) { + case 0: + if (constraint.m_rhs) + s().set_conflict(); + return false; + case 1: { + s().assign_scoped(sat::literal(constraint[0], !constraint.m_rhs)); + s().propagate(false); + return false; + } + case 2: { + /*literal_vector vec(constraint.size()); + for (const auto& v : constraint.m_vars) + vec.push_back(literal(v)); + add_xor_clause(vec, constraint.m_rhs, true);*/ + + /*m_ctx->e_internalize(m_ctx->bool_var2expr(constraint[0])); + m_ctx->e_internalize(m_ctx->bool_var2expr(constraint[1])); + expr* e = m_ctx->mk_eq(m_ctx->bool_var2enode(constraint[0]), m_ctx->bool_var2enode(constraint[1])); + literal l = m_ctx->expr2literal(e); + if (constraint.m_rhs) + l.neg(); + s().add_clause(l, sat::status::th(false, get_id()));*/ + literal l1(constraint[0]); + literal l2(constraint[1]); + if (constraint.m_rhs) { // not equal + s().add_clause(l1, l2, sat::status::th(false, get_id())); + s().add_clause(~l1, ~l2, sat::status::th(false, get_id())); + } + else { // equal + s().add_clause(l1, ~l2, sat::status::th(false, get_id())); + s().add_clause(~l1, l2, sat::status::th(false, get_id())); + } + return false; + } + default: + return true; + } + } + // 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) { unsigned j = 0; @@ -331,29 +380,10 @@ namespace xr { x[j++] = v; } x.shrink(j); - SASSERT(!inconsistent()); - switch (x.size()) { - case 0: - if (x.m_rhs) - s().set_conflict(); - return false; - case 1: { - s().assign_scoped(sat::literal(x[0], !x.m_rhs)); - s().propagate(false); - return false; - } - case 2: { - literal_vector vec(x.size()); - for (const auto& v : x.m_vars) - vec.push_back(literal(v)); - add_xor_clause(vec, x.m_rhs, true); - return false; - } - default: - return true; - } + return add_simple_xor_constraint(x); } + // reset all data-structures. Resets m_xorclauses from m_xorclauses_orig bool solver::clear_gauss_matrices(const bool destruct) { // TODO: Include; ignored for now. Maybe we can ignore the detached clauses /*if (!destruct) { @@ -483,7 +513,8 @@ namespace xr { m_xorclauses = cleaned; } - + + // As the name suggests: Checks if there are (syntactically) equivalent xors and removes all these duplicates void solver::clean_equivalent_xors(vector& txors){ if (!txors.empty()) { for (xor_clause& x: txors) @@ -495,8 +526,8 @@ namespace xr { unsigned sz = 1; unsigned j = 0; for (unsigned i = 1; i < txors.size(); i++) { - auto& jd = txors[j]; - auto& id = txors[i]; + xor_clause& jd = txors[j]; + xor_clause& id = txors[i]; if (jd.m_vars == id.m_vars && jd.m_rhs == id.m_rhs) { jd.merge_clash(id, m_visited, s().num_vars()); jd.m_detached |= id.m_detached; @@ -518,6 +549,7 @@ namespace xr { return sat::justification::mk_ext_justification(level, constraint->to_index()); } + // sort xors, eliminate duplicates, and eliminate negations by flipping rhs void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) { std::sort(ps.begin(), ps.end()); sat::literal p_last = sat::null_literal; @@ -728,7 +760,7 @@ namespace xr { // Remove all watches coming from xor solver // TODO: Differentiate if the watch came from another theory (not xor)!! void solver::clean_occur_from_idx(const literal l) { - vector& ws = s().get_wlist(~l); // the same polarity that was added + vector& ws = s().get_wlist(l); // the same polarity that was added unsigned i = 0, j = 0; const unsigned end = ws.size(); for (; i < end; i++) { diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index ddec48df6..3923fd27f 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -75,6 +75,8 @@ namespace xr { void clean_xors_from_empty(vector& thisxors); unsigned xor_two(xor_clause const* x1_p, xor_clause const* x2_p, bool_var& clash_var); + bool add_simple_xor_constraint(const xor_clause& constraint); + bool inconsistent() const { return s().inconsistent(); } // TODO: CMS watches the literals directly; Z3 their negation. "_neg_" just for now to avoid confusion @@ -83,11 +85,11 @@ namespace xr { } bool is_neg_watched(literal lit, size_t idx) const { - return s().get_wlist(~lit).contains(sat::watched((sat::ext_constraint_idx)idx)); + 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)); + s().get_wlist(lit).erase(sat::watched(idx)); SASSERT(!is_neg_watched(lit, idx)); } @@ -97,10 +99,25 @@ namespace xr { } void watch_neg_literal(literal lit, size_t idx) { - watch_neg_literal(s().get_wlist(~lit), idx); + watch_neg_literal(s().get_wlist(lit), idx); + } + + static std::string toString(literal l) { + return (std::stringstream() << l).str(); + } + + static std::string toString(const literal& l) { + return (std::stringstream() << l).str(); + } + + static std::string toString(const literal_vector& l) { + return (std::stringstream() << l).str(); + } + + static std::string toString(const bool_var_vector & l) { + return (std::stringstream() << l).str(); } - public: solver(euf::solver& ctx); solver(ast_manager& m, euf::theory_id id);