mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

debug dio

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-01 11:32:00 -08:00
parent aa57ee7b62
commit 7cfecaa0b4
4 changed files with 83 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1463,10 +1463,9 @@ namespace lp {
}
// we have m_espace and m_lspace filled with an lra_term and the variables are substituted by S and fresh
lia_move tighten_bounds_for_term_column_bp() {
return lia_move::undef;
std::cout << "tighten_bounds_for_term_column_bp\n";
lia_move tighten_bounds_for_term_column_bp(unsigned j) {
remove_fresh_from_espace();
// transform to lar variables
for (auto & p: m_espace.m_data) p.m_j = local_to_lar_solver(p.var()); // have to restore it for the cleanup to work
TRACE("dio",
@ -1479,21 +1478,23 @@ namespace lp {
m_prop_bounds.clear();
bound_analyzer_on_row<std_vector<iv>, dioph_eq::imp>::analyze_row(m_espace.m_data, impq(- m_c), *this);
lia_move r = lia_move::undef;
bool change = false;
u_dependency * fixed_dep = explain_fixed_in_meta_term(m_lspace.m_data); // not efficient : todo
u_dependency * dep = explain_fixed_in_meta_term(m_lspace.m_data); // not efficient : todo
dep = lra.join_deps(explain_fixed(lra.get_term(j)), dep);
if (is_fixed(j)) dep = lra.join_deps(dep, lra.get_bound_constraint_witnesses_for_column(j));
for (auto& pb: m_prop_bounds) {
pb.m_dep = lra.join_deps(pb.m_dep, fixed_dep);
pb.m_dep = lra.join_deps(pb.m_dep, dep);
if (update_bound(pb)) {
change = true;
TRACE("dio", tout << "change after update_bound pb.m_j:" << pb.m_j << "\n";);
auto st = lra.find_feasible_solution();
if (st == lp_status::INFEASIBLE) {
lra.get_infeasibility_explanation(m_infeas_explanation);
TRACE("dio", tout << "inf explanation:\n"; lra.print_explanation(tout, m_infeas_explanation););
r = lia_move::conflict;
break;
}
TRACE("dio", tout << "lra is feasible\n";);
}
}
if (change) {
auto st = lra.find_feasible_solution();
if (st == lp_status::INFEASIBLE) {
lra.get_infeasibility_explanation(m_infeas_explanation);
r = lia_move::conflict;
}
}
for (auto & p: m_espace.m_data) p.m_j = lar_solver_to_local(p.var());
return r;
}
@ -1501,7 +1502,7 @@ namespace lp {
lia_move tighten_bounds_for_term_column(unsigned j) {
auto r = tighten_bounds_for_term_column_gcd(j);
if (r == lia_move::undef)
r = tighten_bounds_for_term_column_bp();
r = tighten_bounds_for_term_column_bp(j);
return r;
}
@ -1513,7 +1514,12 @@ namespace lp {
SASSERT(get_extended_term_value(term_to_tighten).is_zero() && all_vars_are_int(term_to_tighten));
// q is the queue of variables that can be substituted in term_to_tighten
protected_queue q;
TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;);
TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;
for( const auto& p : term_to_tighten) {
lra.print_column_info(p.var(), tout);
}
);
init_substitutions(term_to_tighten, q);
if (q.empty()) // todo: maybe still go ahead and process it?
return lia_move::undef;
@ -1526,7 +1532,7 @@ namespace lp {
subs_with_S_and_fresh(q);
SASSERT(subs_invariant(term_to_tighten));
mpq g = gcd_of_coeffs(m_espace.m_data, true);
TRACE("dioph_eq", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
TRACE("dio", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
if (g.is_one())
return lia_move::undef;
@ -1734,10 +1740,11 @@ namespace lp {
}
// return true iff the column bound has been changed
bool update_bound(const prop_bound& pb) {
lra.update_column_type_and_bound(pb.m_j, get_bound_kind(pb), pb.m_bound, pb.m_dep);
if (lra.column_is_fixed(pb.m_j)) std::cout << "new fixed " << pb.m_j << "\n";
return lra.columns_with_changed_bounds().contains(pb.m_j);
bool update_bound(const prop_bound& pb) {
TRACE("dio", tout << "pb: " << "x" << pb.m_j << ", low:" << pb.m_is_low << " , strict:" << pb.m_strict << " , bound:" << pb.m_bound << "\n"; lra.print_column_info(pb.m_j, tout, true););
bool r = lra.update_column_type_and_bound(pb.m_j, get_bound_kind(pb), pb.m_bound, pb.m_dep);
TRACE("dio", tout << "after: "; lra.print_column_info(pb.m_j, tout);tout <<"return " << r << "\n";);
return r;
}
bool row_has_int_inf(unsigned ei) {
@ -1767,10 +1774,12 @@ namespace lp {
tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":"
<< rs << std::endl;);
rs = (rs - m_c) / g;
TRACE("dio", tout << "(rs - m_c) / g:" << rs << std::endl;);
TRACE("dio", tout << "((rs - m_c) / g):" << rs << std::endl;);
if (!rs.is_int()) {
if (tighten_bound_kind(g, j, rs, is_upper, b_dep))
return lia_move::conflict;
} else {
TRACE("dio", tout << "no improvement in the bound\n";);
}
}

50
src/math/lp/lar_solver.cpp
View file

@ -1867,14 +1867,14 @@ namespace lp {
}
}
void lar_solver::update_column_type_and_bound(unsigned j,
bool lar_solver::update_column_type_and_bound(unsigned j,
const mpq& right_side,
constraint_index constr_index) {
TRACE("lar_solver_feas", tout << "j = " << j << " was " << (this->column_is_feasible(j)?"feas":"non-feas") << std::endl;);
m_constraints.activate(constr_index);
lconstraint_kind kind = m_constraints[constr_index].kind();
u_dependency* dep = m_constraints[constr_index].dep();
update_column_type_and_bound(j, kind, right_side, dep);
return update_column_type_and_bound(j, kind, right_side, dep);
}
@ -1956,7 +1956,8 @@ namespace lp {
}
ls.add_var_bound(tv, c.kind(), c.rhs());
}
void lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
// return true iff a bound has been changed or or the criss-crossed bounds have been found
bool lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
// SASSERT(validate_bound(j, kind, right_side, dep));
TRACE(
"lar_solver_feas",
@ -1972,11 +1973,12 @@ namespace lp {
});
bool was_fixed = column_is_fixed(j);
mpq rs = adjust_bound_for_int(j, kind, right_side);
bool r;
if (column_has_upper_bound(j))
update_column_type_and_bound_with_ub(j, kind, rs, dep);
r = update_column_type_and_bound_with_ub(j, kind, rs, dep);
else
update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
r = update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
if (!was_fixed && column_is_fixed(j) && m_fixed_var_eh)
m_fixed_var_eh(j);
@ -1987,6 +1989,7 @@ namespace lp {
TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j) ? "feas" : "non-feas") << ", and " << (this->column_is_bounded(j) ? "bounded" : "non-bounded") << std::endl;);
if (m_update_column_bound_callback)
m_update_column_bound_callback(j);
return r;
}
void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
@ -2021,27 +2024,27 @@ namespace lp {
}
};
void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
bool lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
SASSERT(column_has_upper_bound(j));
if (column_has_lower_bound(j)) {
update_bound_with_ub_lb(j, kind, right_side, dep);
return update_bound_with_ub_lb(j, kind, right_side, dep);
}
else {
update_bound_with_ub_no_lb(j, kind, right_side, dep);
return update_bound_with_ub_no_lb(j, kind, right_side, dep);
}
}
void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
bool lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
SASSERT(!column_has_upper_bound(j));
if (column_has_lower_bound(j)) {
update_bound_with_no_ub_lb(j, kind, right_side, dep);
return update_bound_with_no_ub_lb(j, kind, right_side, dep);
}
else {
update_bound_with_no_ub_no_lb(j, kind, right_side, dep);
return update_bound_with_no_ub_no_lb(j, kind, right_side, dep);
}
}
void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
bool lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed ||
m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed);
@ -2057,7 +2060,7 @@ namespace lp {
set_crossed_bounds_column_and_deps(j, true, dep);
}
else {
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return false;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, dep);
insert_to_columns_with_changed_bounds(j);
@ -2072,9 +2075,7 @@ namespace lp {
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
set_crossed_bounds_column_and_deps(j, false, dep);
} else {
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
}
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) return false;
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
set_lower_bound_witness(j, dep);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed);
@ -2107,9 +2108,10 @@ namespace lp {
numeric_pair<mpq> const& hi = m_mpq_lar_core_solver.m_r_upper_bounds[j];
if (lo == hi)
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
return true;
}
void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
bool lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
@ -2136,7 +2138,7 @@ namespace lp {
case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound);
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
return;
return false;
}
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
set_lower_bound_witness(j, dep);
@ -2161,9 +2163,10 @@ namespace lp {
default:
UNREACHABLE();
}
return true;
}
void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
bool lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
mpq y_of_bound(0);
@ -2174,7 +2177,7 @@ namespace lp {
case LE:
{
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return false;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, dep);
insert_to_columns_with_changed_bounds(j);
@ -2216,9 +2219,10 @@ namespace lp {
default:
UNREACHABLE();
}
return true;
}
void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
bool lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j));
mpq y_of_bound(0);
@ -2255,6 +2259,7 @@ namespace lp {
UNREACHABLE();
}
insert_to_columns_with_changed_bounds(j);
return true;
}
lpvar lar_solver::to_column(unsigned ext_j) const {
@ -2508,7 +2513,6 @@ namespace lp {
u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
SASSERT(bdep != nullptr);
m_crossed_bounds_deps = m_dependencies.mk_join(bdep, dep);
insert_to_columns_with_changed_bounds(j);
}
void lar_solver::collect_more_rows_for_lp_propagation(){

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

@ -156,19 +156,19 @@ class lar_solver : public column_namer {
void add_constraint_to_validate(lar_solver& ls, constraint_index ci);
bool m_validate_blocker = false;
void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
void update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
bool update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
public:
bool validate_blocker() const { return m_validate_blocker; }
bool & validate_blocker() { return m_validate_blocker; }
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
private:
void require_nbasis_sort() { m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; }
void update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
bool update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void register_in_fixed_var_table(unsigned, unsigned&);
void remove_non_fixed_from_fixed_var_table();
constraint_index add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side);
@ -614,11 +614,12 @@ public:
}
inline bool column_has_term(lpvar j) const { return m_columns[j].term() != nullptr; }
std::ostream& print_column_info(unsigned j, std::ostream& out) const {
std::ostream& print_column_info(unsigned j, std::ostream& out, bool print_expl = false) const {
m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
if (column_has_term(j))
print_term_as_indices(get_term(j), out) << "\n";
display_column_explanation(out, j);
if (print_expl)
display_column_explanation(out, j);
return out;
}
@ -627,10 +628,18 @@ public:
svector<unsigned> vs1, vs2;
m_dependencies.linearize(ul.lower_bound_witness(), vs1);
m_dependencies.linearize(ul.upper_bound_witness(), vs2);
if (!vs1.empty())
out << "lo: " << vs1;
if (!vs2.empty())
out << "hi: " << vs2;
if (!vs1.empty()) {
out << " lo:\n";
for (unsigned ci : vs1) {
display_constraint(out, ci) << "\n";
}
}
if (!vs2.empty()) {
out << " hi:\n";
for (unsigned ci : vs2) {
display_constraint(out, ci) << "\n";
}
}
if (!vs1.empty() || !vs2.empty())
out << "\n";
return out;

2
src/math/lp/numeric_pair.h
View file

@ -239,6 +239,8 @@ struct numeric_pair {
void neg() { x.neg(); y.neg(); }
std::string to_string() const {
if (y.is_zero())
return T_to_string(x);
return std::string("(") + T_to_string(x) + ", " + T_to_string(y) + ")";
}