From 59e2dab69a363b5b647f29b415a149c366948999 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 22 Aug 2024 08:40:41 -1000 Subject: [PATCH] create a conflict explanation Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 13 +++++++------ src/math/lp/dioph_eq.h | 1 + src/math/lp/int_solver.cpp | 3 ++- src/math/lp/lar_solver.h | 8 ++++++++ src/math/lp/lp_bound_propagator.h | 15 ++++----------- 5 files changed, 22 insertions(+), 18 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 0dbe7c5c8..944c5414b 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -211,7 +211,7 @@ namespace lp { init(); while(m_f.size()) { if (!normalize_by_gcd()) - return lia_move::unsat; + return lia_move::conflict; rewrite_eqs(); } return lia_move::sat; @@ -298,11 +298,12 @@ namespace lp { remove_fresh_variables(m_eprime[p.j()].m_e); } u_dependency* dep = nullptr; - for (const auto & p : ep.m_l) { - if (lra.column_is_fixed(p.j())) { - lra.explain_fixed_column(p.j(), ex); - } - } + for (const auto & pl : ep.m_l) + for (const auto & p : m_eprime[pl.j()].m_e) + if (lra.column_is_fixed(p.j())) + lra.explain_fixed_column(p.j(), ex); + + TRACE("dioph_eq", lra.print_expl(tout, ex);); } void remove_fresh_variables(term_o& t) { // TODO implement diff --git a/src/math/lp/dioph_eq.h b/src/math/lp/dioph_eq.h index 628453d60..1c5cdf36f 100644 --- a/src/math/lp/dioph_eq.h +++ b/src/math/lp/dioph_eq.h @@ -17,6 +17,7 @@ Revision History: --*/ #pragma once #include "math/lp/lia_move.h" +#include "math/lp/explanation.h" namespace lp { diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 7ebda83cb..fcf1e292f 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -168,8 +168,9 @@ namespace lp { dioph_eq de(lia); lia_move r = de.check(); - if (r == lia_move::unsat) { + if (r == lia_move::conflict) { de.explain(*this->m_ex); + return lia_move::conflict; } else if (r == lia_move::sat) { NOT_IMPLEMENTED_YET(); } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 625839c92..00a4f9c06 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -591,6 +591,14 @@ public: } return dep; } + + std::ostream& print_expl(std::ostream& out, const explanation& exp) const { + for (auto p : exp) + constraints().display( + out, [this](lpvar j) { return get_variable_name(j); }, p.ci()); + return out; + } + void explain_fixed_column(unsigned j, explanation& ex); u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); } inline constraint_set const& constraints() const { return m_constraints; } diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index d45d4cc7c..9da65db04 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -213,20 +213,13 @@ public: m_visited_rows.reset(); } - std::ostream& print_expl(std::ostream& out, const explanation& exp) const { - for (auto p : exp) - lp().constraints().display( - out, [this](lpvar j) { return lp().get_variable_name(j); }, p.ci()); - return out; - } - bool add_eq_on_columns(const explanation& exp, lpvar je, lpvar ke, bool is_fixed) { lp_assert(je != ke && is_int(je) == is_int(ke)); lp_assert(ival(je) == ival(ke)); TRACE("eq", tout << "reported idx " << je << ", " << ke << "\n"; - print_expl(tout, exp); + lp().print_expl(tout, exp); tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";); bool added = m_imp.add_eq(je, ke, exp, is_fixed); @@ -257,7 +250,7 @@ public: TRACE("eq", tout << lp().get_row(row) << std::endl); for (const auto& c : lp().get_row(row)) if (lp().column_is_fixed(c.var())) - explain_fixed_column(c.var(), ex); + lp().explain_fixed_column(c.var(), ex); } unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) { @@ -265,7 +258,7 @@ public: TRACE("eq", tout << lp().get_row(row) << std::endl); for (const auto& c : lp().get_row(row)) { if (lp().column_is_fixed(c.var())) { - explain_fixed_column(c.var(), ex); + lp().explain_fixed_column(c.var(), ex); } else if (lp().is_base(c.var())) { base = c.var(); @@ -357,7 +350,7 @@ public: ); explanation ex; explain_fixed_in_row(row_index, ex); - explain_fixed_column(j, ex); + lp().explain_fixed_column(j, ex); add_eq_on_columns(ex, j, v_j, true); }