From 662019ee171881018f2bf4e7505a62104b4b7e8c Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Mon, 5 Dec 2022 07:52:56 +0100 Subject: [PATCH] Fixed decision-level (again) --- src/sat/smt/xor_gaussian.cpp | 12 ++++++------ src/sat/smt/xor_solver.cpp | 10 +++++----- src/sat/smt/xor_solver.h | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp index aa837e48d..91e29b6d7 100644 --- a/src/sat/smt/xor_gaussian.cpp +++ b/src/sat/smt/xor_gaussian.cpp @@ -598,7 +598,7 @@ bool EGaussian::find_truths( << "mat[" << matrix_no << "] find_truths\n" << "-> row: " << row_n << "\n" << "-> var: " << var+1 << "\n" - << "-> dec lev:" << m_solver.s().search_lvl()); + << "-> dec lev:" << m_solver.s().scope_lvl()); SASSERT(row_n < m_num_rows); SASSERT(satisfied_xors.size() > row_n); @@ -641,7 +641,7 @@ bool EGaussian::find_truths( xor_reasons[row_n].m_must_recalc = true; xor_reasons[row_n].m_propagated = sat::null_literal; - gqd.conflict = m_solver.mk_justification(m_solver.s().search_lvl(), matrix_no, row_n); + gqd.conflict = m_solver.mk_justification(m_solver.s().scope_lvl(), matrix_no, row_n); gqd.status = gauss_res::confl; TRACE("xor", tout << "--> conflict";); @@ -788,7 +788,7 @@ void EGaussian::update_cols_vals_set(bool force) { void EGaussian::prop_lit(const gauss_data& gqd, unsigned row_i, literal ret_lit_prop) { unsigned level; - if (gqd.currLevel == m_solver.s().search_lvl()) + if (gqd.currLevel == m_solver.s().scope_lvl()) level = gqd.currLevel; else level = get_max_level(gqd, row_i); @@ -870,7 +870,7 @@ void EGaussian::eliminate_column(unsigned p, gauss_data& gqd) { xor_reasons[row_i].m_must_recalc = true; xor_reasons[row_i].m_propagated = sat::null_literal; - gqd.conflict = m_solver.mk_justification(m_solver.s().search_lvl(), matrix_no, row_i); + gqd.conflict = m_solver.mk_justification(m_solver.s().scope_lvl(), matrix_no, row_i); gqd.status = gauss_res::confl; break; @@ -982,7 +982,7 @@ void EGaussian::check_no_prop_or_unsat_rows() { tout << " matrix no: " << matrix_no << "\n" << " row: " << row << "\n" << " non-resp var: " << row_to_var_non_resp[row] + 1 << "\n" - << " dec level: " << m_solver.s().search_lvl() << "\n"; + << " dec level: " << m_solver.s().scope_lvl() << "\n"; for (unsigned var = 0; var < m_solver.s().num_vars(); var++) for (const auto& w : m_solver.m_gwatches[var]) if (w.matrix_num == matrix_no && w.row_n == row) @@ -1042,7 +1042,7 @@ void EGaussian::check_invariants() { if (!initialized) return; check_tracked_cols_only_one_set(); check_no_prop_or_unsat_rows(); - TRACE("xor", tout << "mat[" << matrix_no << "] " << "Checked invariants. Dec level: " << m_solver.s().search_lvl() << "\n";); + TRACE("xor", tout << "mat[" << matrix_no << "] " << "Checked invariants. Dec level: " << m_solver.s().scope_lvl() << "\n";); } bool EGaussian::check_row_satisfied(unsigned row) { diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index c38643b30..a423c7034 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -82,7 +82,7 @@ namespace xr { } } - void solver::add_xor_clause(const sat::literal_vector& lits, bool rhs, const bool attach) { + void solver::add_xor_clause(const literal_vector& lits, bool rhs, const bool attach) { // TODO: make overload in which "lits" ==> svector; however, first implement missing function "add_xor_clause_inter_cleaned_cut" if (s().inconsistent()) return; @@ -90,8 +90,8 @@ namespace xr { SASSERT(!attach || m_prop_queue_head == m_prop_queue.size()); SASSERT(s().at_search_lvl()); - sat::literal_vector ps(lits); - for (sat::literal& lit: ps) { + literal_vector ps(lits); + for (literal& lit: ps) { if (lit.sign()) { rhs ^= true; lit.neg(); @@ -559,9 +559,9 @@ namespace xr { } // sort xors, eliminate duplicates, and eliminate negations by flipping rhs - void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) { + void solver::clean_xor_no_prop(literal_vector & ps, bool & rhs) { std::sort(ps.begin(), ps.end()); - sat::literal p_last = sat::null_literal; + literal p_last = sat::null_literal; unsigned j = 0; for (auto p : ps) { SASSERT(!p.sign()); diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index 1e5ea5619..d5324e89e 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -68,10 +68,10 @@ namespace xr { bool xor_has_interesting_var(const xor_clause& x); - void clean_xor_no_prop(sat::literal_vector& ps, bool& rhs); + void clean_xor_no_prop(literal_vector& ps, bool& rhs); void add_every_combination_xor(const sat::literal_vector& lits, const bool attach); - void add_xor_clause(const sat::literal_vector& lits, bool rhs, const bool attach); + void add_xor_clause(const literal_vector& lits, bool rhs, const bool attach); void clean_occur_from_idx(const literal l); void clean_xors_from_empty(vector& thisxors);