diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp index 86caa4fdb..87ff1b588 100644 --- a/src/sat/smt/xor_gaussian.cpp +++ b/src/sat/smt/xor_gaussian.cpp @@ -400,7 +400,8 @@ static void print_matrix(ostream& out, PackedMatrix& mat) { // Applies Gaussian-Jordan elimination (search level). This function does not add conflicts/propagate/... Just reduces the matrix void EGaussian::eliminate() { - // TODO: Why twice? gauss_jordan_elim + SASSERT(m_solver.s().at_search_lvl()); + unsigned end_row = num_rows; unsigned rowI = 0; unsigned row_i = 0; diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 9e4c181e5..d4df0ab16 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -94,6 +94,7 @@ namespace xr { rhs ^= true; lit.neg(); } + s().set_external(lit.var()); } clean_xor_no_prop(ps, rhs); @@ -131,11 +132,10 @@ namespace xr { if (m_prop_queue_head == m_prop_queue.size()) return false; force_push(); - m_ctx->push(value_trail(m_prop_queue_head)); for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) { sat::literal const p = m_prop_queue[m_prop_queue_head]; sat::justification conflict = gauss_jordan_elim(p, m_num_scopes); - if (conflict.is_none()) { + if (!conflict.is_none()) { m_prop_queue_head = m_prop_queue.size(); s().set_conflict(conflict); } @@ -238,6 +238,7 @@ namespace xr { void solver::push_core() { m_prop_queue_lim.push_back(m_prop_queue.size()); + m_prop_queue_head_queue.push_back(m_prop_queue_head); //m_justifications_lim.push_back(m_justifications.size()); } @@ -247,6 +248,9 @@ namespace xr { m_prop_queue.shrink(m_prop_queue_lim[old_sz]); m_prop_queue_lim.shrink(old_sz); + m_prop_queue_head = m_prop_queue_head_queue[old_sz]; + m_prop_queue_head_queue.shrink(old_sz); + /*old_sz = m_justifications_lim.size() - num_scopes; unsigned lim = m_justifications_lim[old_sz]; for (unsigned i = m_justifications.size(); i > lim; i--) { @@ -583,6 +587,11 @@ namespace xr { if (xors.empty()) return !s().inconsistent(); + if (s().is_incremental()) { // TODO: What should we do in this case? + clean_xors_from_empty(xors); + return !s().inconsistent(); + } + if (m_occ_cnt.size() != s().num_vars()) { m_occ_cnt.clear(); m_occ_cnt.resize(s().num_vars(), 0); @@ -613,25 +622,7 @@ namespace xr { } } - s().init_visited(); - - // We can only eliminate variables that are non-external and not used in clauses. - // Don't XOR together over variables that are external - for (unsigned i = 0; i < s().num_vars(); i++) - if (s().is_external(i)) - s().mark_visited(i); - - // Don't XOR together over variables that are in irredundant clauses - // learned clauses are redundant. - for (unsigned i = 0; i < 2 * s().num_vars(); i++) - for (const auto& w: s().get_wlist(i)) - if (w.is_binary_clause() && !w.is_learned()) - s().mark_visited(w.get_literal().var()); - - for (const auto& cl: s().clauses()) - if (!cl->is_learned()) - for (literal l: *cl) - s().mark_visited(l.var()); + mark_non_removable_atoms(); // until fixedpoint bool changed = true; @@ -731,8 +722,6 @@ namespace xr { return !s().inconsistent(); } - - // Removes all xor clauses that do not contain any variables // (and have rhs = false; i.e., are trivially satisfied) and move them to unused void solver::clean_xors_from_empty(vector& thisxors) { @@ -748,6 +737,44 @@ namespace xr { thisxors.shrink(j); } + // marks all elements that may NOT be removed by merging xors + void solver::mark_non_removable_atoms() { + s().init_visited(); + + // We can only eliminate variables that are non-external and not used in clauses. + // Don't XOR together over variables that are external + for (bool_var v = 0; v < s().num_vars(); v++) { + if (!s().is_external(v)) // We can ignore this case, as all variables in xor-clauses are marked as external for sure + continue; + if (is_theory_atom(v)) + s().mark_visited(v); + } + + // Don't XOR together over variables that are in irredundant clauses + // learned clauses are redundant. + for (unsigned i = 0; i < 2 * s().num_vars(); i++) + for (const auto& w: s().get_wlist(i)) + if (w.is_binary_clause() && !w.is_learned()) + s().mark_visited(w.get_literal().var()); + + for (const auto& cl: s().clauses()) + if (!cl->is_learned()) + for (literal l: *cl) + s().mark_visited(l.var()); + } + + bool solver::is_theory_atom(bool_var v) const { + if (m_ctx == nullptr) + return false; // there is no other solver + + euf::enode* n = m_ctx->bool_var2enode(v); + if (!n) + return false; + + auto th_vars = euf::enode_th_vars(n); + return std::any_of(th_vars.begin(), th_vars.end(), [&](const euf::th_var_list& thv) { return m_ctx->fid2solver(thv.get_id()); }); + } + // Merge two xor clauses; the resulting clause is in m_tmp_vars_xor_two and the variable where it was glued is in clash_var // returns 0 if no common variable was found, 1 if there was exactly one and 2 if there are more // only 1 is successful diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index 405e726a4..09dd37d61 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -31,7 +31,9 @@ namespace xr { literal_vector m_prop_queue; unsigned_vector m_prop_queue_lim; + unsigned m_prop_queue_head = 0; + unsigned_vector m_prop_queue_head_queue; // ptr_vector m_justifications; // unsigned_vector m_justifications_lim; @@ -73,6 +75,9 @@ namespace xr { void clean_occur_from_idx(const literal l); void clean_xors_from_empty(vector& thisxors); + + bool is_theory_atom(bool_var v) const; + void mark_non_removable_atoms(); 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);