mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

create a conflict explanation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-08-22 08:40:41 -10:00 • committed by Lev Nachmanson
parent 52653e6e43
commit 59e2dab69a
5 changed files with 22 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/lp/dioph_eq.cpp
View file

@ -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

1
src/math/lp/dioph_eq.h
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#pragma once
#include "math/lp/lia_move.h"
#include "math/lp/explanation.h"
namespace lp {

3
src/math/lp/int_solver.cpp
View file

@ -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();
}

8
src/math/lp/lar_solver.h
View file

@ -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; }

15
src/math/lp/lp_bound_propagator.h
View file

@ -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);
}