mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

debug dio

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-09-26 13:59:00 -07:00 committed by Lev Nachmanson
parent 798f0e2e8a
commit 89e4f59df2
1 changed files with 678 additions and 654 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -7,7 +7,7 @@
namespace lp { namespace lp {
// This class represents a term with an added constant number c, in form sum {x_i*a_i} + c. // This class represents a term with an added constant number c, in form sum {x_i*a_i} + c.
int global_max_change = 100000; // 9 , 10
class dioph_eq::imp { class dioph_eq::imp {
class term_o:public lar_term { class term_o:public lar_term {
mpq m_c; mpq m_c;
@ -132,6 +132,8 @@ namespace lp {
public: public:
int_solver& lia; int_solver& lia;
lar_solver& lra; lar_solver& lra;
explanation m_infeas_explanation;
// we start assigning with UINT_MAX and go down, print it as l(UINT_MAX - m_last_fresh_x_var) // we start assigning with UINT_MAX and go down, print it as l(UINT_MAX - m_last_fresh_x_var)
unsigned m_last_fresh_x_var = UINT_MAX; unsigned m_last_fresh_x_var = UINT_MAX;
@ -162,6 +164,7 @@ namespace lp {
unsigned n_of_rows = lra.A_r().row_count(); unsigned n_of_rows = lra.A_r().row_count();
unsigned fn = 0; unsigned fn = 0;
m_conflict_index = -1; m_conflict_index = -1;
m_infeas_explanation.clear();
auto all_vars_are_int = [this](const auto& row) { auto all_vars_are_int = [this](const auto& row) {
for (const auto& p : row) { for (const auto& p : row) {
@ -316,7 +319,12 @@ namespace lp {
} }
} }
lia_move tighten_with_S_push_pop() {
lra.push();
lia_move ret = tighten_with_S();
lra.pop();
return ret;
}
lia_move tighten_with_S() { lia_move tighten_with_S() {
// following the pattern of int_cube // following the pattern of int_cube
@ -324,14 +332,18 @@ namespace lp {
for (unsigned j = 0; j < lra.column_count(); j++) { for (unsigned j = 0; j < lra.column_count(); j++) {
if (!lra.column_has_term(j) || lra.column_is_free(j) || if (!lra.column_has_term(j) || lra.column_is_free(j) ||
lra.column_is_fixed(j) || !lia.column_is_int(j)) continue; lra.column_is_fixed(j) || !lia.column_is_int(j)) continue;
if (tighten_bounds_for_column(j)) if (tighten_bounds_for_column(j)) {
change++; change++;
} }
}
if (!change) if (!change)
return lia_move::undef; return lia_move::undef;
std::cout << "change " << change << std::endl;
auto st = lra.find_feasible_solution(); auto st = lra.find_feasible_solution();
if (st != lp::lp_status::FEASIBLE && st != lp::lp_status::OPTIMAL) { if (st != lp::lp_status::FEASIBLE && st != lp::lp_status::OPTIMAL) {
std::cout << "report conflict\n"; lra.get_infeasibility_explanation(m_infeas_explanation);
std::cout << "tighten_with_S: infeasible\n";
return lia_move::conflict; return lia_move::conflict;
} }
return lia_move::undef; return lia_move::undef;
@ -372,6 +384,10 @@ namespace lp {
bool is_strict; bool is_strict;
bool change = false; bool change = false;
u_dependency *b_dep = nullptr; u_dependency *b_dep = nullptr;
if (global_max_change <= 0) {
return change;
}
if (lra.has_upper_bound(j, b_dep, rs, is_strict)) { if (lra.has_upper_bound(j, b_dep, rs, is_strict)) {
TRACE("dioph_eq", tout << "tighten upper bound for x" << j << " with rs:" << rs << std::endl;); TRACE("dioph_eq", tout << "tighten upper bound for x" << j << " with rs:" << rs << std::endl;);
rs = rs - t.c(); rs = rs - t.c();
@ -381,8 +397,13 @@ namespace lp {
if (!rs.is_int() || !t.c().is_zero()) { if (!rs.is_int() || !t.c().is_zero()) {
tighten_bound_for_term(t, g, j, lra.mk_join(dep, b_dep), rs, true); tighten_bound_for_term(t, g, j, lra.mk_join(dep, b_dep), rs, true);
change = true; change = true;
global_max_change--;
} }
} }
if (global_max_change <= 0) {
return change;
}
if (lra.has_lower_bound(j, b_dep, rs, is_strict)) { if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
TRACE("dioph_eq", tout << "tighten lower bound for x" << j << " with rs:" << rs << std::endl;); TRACE("dioph_eq", tout << "tighten lower bound for x" << j << " with rs:" << rs << std::endl;);
rs = rs - t.c(); rs = rs - t.c();
@ -392,6 +413,7 @@ namespace lp {
if (!rs.is_int()|| !t.c().is_zero()) { if (!rs.is_int()|| !t.c().is_zero()) {
tighten_bound_for_term(t, g, j, lra.mk_join(b_dep, dep), rs, false); tighten_bound_for_term(t, g, j, lra.mk_join(b_dep, dep), rs, false);
change = true; change = true;
global_max_change--;
} }
} }
return change; return change;
@ -423,7 +445,7 @@ namespace lp {
rewrite_eqs(); rewrite_eqs();
} }
TRACE("dioph_eq", print_S(tout);); TRACE("dioph_eq", print_S(tout););
lia_move ret = tighten_with_S(); lia_move ret = tighten_with_S_push_pop();
if (ret == lia_move::conflict) { if (ret == lia_move::conflict) {
return lia_move::conflict; return lia_move::conflict;
} }
@ -586,7 +608,9 @@ namespace lp {
void explain(explanation& ex) { void explain(explanation& ex) {
if (m_conflict_index == -1) { if (m_conflict_index == -1) {
SASSERT(!(lra.get_status() == lp_status::FEASIBLE || lra.get_status() == lp_status::OPTIMAL)); SASSERT(!(lra.get_status() == lp_status::FEASIBLE || lra.get_status() == lp_status::OPTIMAL));
lra.get_infeasibility_explanation(ex); for (auto ci: m_infeas_explanation) {
ex.push_back(ci.ci());
}
return; return;
} }
SASSERT(ex.empty()); SASSERT(ex.empty());