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

before getting explanations for monomials upper and low bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-06 16:13:49 -07:00
parent 02133bbcc5
commit 6a6cb3822c
5 changed files with 26 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -224,29 +224,6 @@ void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagat
}
void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) {
unsigned i = ib.m_row_or_term_index;
int bound_sign = ib.m_is_lower_bound? 1: -1;
int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
unsigned bound_j = ib.m_j;
if (is_term(bound_j)) {
bound_j = m_var_register.external_to_local(bound_j);
}
for (auto const& r : A_r().m_rows[i]) {
unsigned j = r.var();
if (j == bound_j) continue;
mpq const& a = r.get_val();
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;
const ul_pair & ul = m_columns_to_ul_pairs[j];
// todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
lp_assert(is_valid(witness));
bp.consume(a, witness);
}
// lp_assert(implied_bound_is_correctly_explained(ib, explanation));
}
bool lar_solver::term_is_used_as_row(unsigned term) const {
lp_assert(is_term(term));

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

@ -315,10 +315,6 @@ public:
void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset);
void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp);
bool term_is_used_as_row(unsigned term) const;
void propagate_bounds_on_terms(lp_bound_propagator & bp);

24
src/math/lp/lp_bound_propagator.cpp
View file

@ -114,4 +114,28 @@ void lp_bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool co
}
}
}
void lp_bound_propagator::explain_implied_bound(implied_bound & ib) {
unsigned i = ib.m_row_or_term_index;
int bound_sign = ib.m_is_lower_bound? 1: -1;
int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
unsigned bound_j = ib.m_j;
if (m_lar_solver.is_term(bound_j)) {
bound_j = m_lar_solver.m_var_register.external_to_local(bound_j);
}
for (auto const& r : m_lar_solver.A_r().m_rows[i]) {
unsigned j = r.var();
if (j == bound_j) continue;
mpq const& a = r.get_val();
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;
const ul_pair & ul = m_lar_solver.m_columns_to_ul_pairs[j];
// todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
lp_assert(is_valid(witness));
consume(a, witness);
}
// lp_assert(implied_bound_is_correctly_explained(ib, explanation));
}
}

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

@ -32,6 +32,7 @@ public:
lp::lconstraint_kind kind,
const rational & bval) {return true;}
unsigned number_of_found_bounds() const { return m_ibounds.size(); }
void explain_implied_bound(implied_bound & ib);
virtual void consume(mpq const& v, lp::constraint_index j) = 0;
};
}

2
src/smt/theory_lra.cpp
View file

@ -2375,7 +2375,7 @@ public:
m_params.reset();
m_explanation.clear();
local_bound_propagator bp(*this);
lp().explain_implied_bound(be, bp);
bp.explain_implied_bound(be);
}
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1);