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

Browse source
This commit is contained in:
Lev Nachmanson 2023-09-16 13:54:14 -07:00
parent c240f62ca8
commit 77e56b0a69
5 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -319,6 +319,7 @@ private:
} }
} }
static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
auto& lar = bp->lp(); auto& lar = bp->lp();
int bound_sign = (is_lower_bound ? 1 : -1); int bound_sign = (is_lower_bound ? 1 : -1);
int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;

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

@ -36,7 +36,7 @@ class implied_bound {
std::function<u_dependency*(int *)> m_explain_bound = nullptr; std::function<u_dependency*(int *)> m_explain_bound = nullptr;
public: public:
// s is expected to be the pointer to lp_bound_propagator. // s is expected to be the pointer to lp_bound_propagator.
u_dependency* explain(int * s) const { return m_explain_bound(s); } u_dependency* explain_implied(int * s) const { return m_explain_bound(s); }
void set_explain(std::function<u_dependency*(int *)> f) { m_explain_bound = f; } void set_explain(std::function<u_dependency*(int *)> f) { m_explain_bound = f; }
lconstraint_kind kind() const { lconstraint_kind kind() const {
lconstraint_kind k = m_is_lower_bound? GE : LE; lconstraint_kind k = m_is_lower_bound? GE : LE;

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

@ -311,9 +311,9 @@ class lar_solver : public column_namer {
template <typename T> template <typename T>
void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) { void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
u_dependency* dep = ib.explain((int*)&bp); u_dependency* dep = ib.explain_implied((int*)&bp);
for (auto ci : flatten(dep)) for (auto ci : flatten(dep))
bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients bp.consume(mpq(1), ci); // TODO: flatten should provide the coefficients
/* /*
if (ib.m_is_monic) { if (ib.m_is_monic) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();

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

@ -137,14 +137,18 @@ private:
return n_of_non_fixed <= 1; return n_of_non_fixed <= 1;
} }
void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) { void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);}); auto lambda = [zero_var](int* s) {
add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);}); return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);
};
TRACE("add_bound", lp().print_column_info(zero_var, tout) << std::endl;);
add_lower_bound_monic(monic_var, mpq(0), false, lambda);
add_upper_bound_monic(monic_var, mpq(0), false, lambda);
} }
void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function<u_dependency* (int*)> explain_dep) { void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function<u_dependency* (int*)> explain_dep) {
unsigned k; unsigned k;
TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;);
j = lp().column_to_reported_index(j); j = lp().column_to_reported_index(j);
if (!try_get_value(m_improved_lower_bounds, j, k)) { if (!try_get_value(m_improved_lower_bounds, j, k)) {
m_improved_lower_bounds[j] = m_ibounds.size(); m_improved_lower_bounds[j] = m_ibounds.size();

2
src/sat/smt/arith_solver.cpp
View file

@ -253,7 +253,7 @@ namespace arith {
first = false; first = false;
reset_evidence(); reset_evidence();
m_explanation.clear(); m_explanation.clear();
be.explain((int*)&m_bp); be.explain_implied((int*)&m_bp);
} }
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1); updt_unassigned_bounds(v, -1);