mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove dead code related to nla unit propagation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-09-19 10:56:09 -07:00
parent cf63e75898
commit c5cfd62e0a
6 changed files with 16 additions and 95 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -162,12 +162,12 @@ private:
void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function<u_dependency* (int*)> explain_dep) {
TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;);
j = lp().column_to_reported_index(j);
auto *e = m_improved_lower_bounds.find_core(j);
if (!e) {
unsigned k;
if (!m_improved_lower_bounds.find(j, k)) {
m_improved_lower_bounds.insert(j,static_cast<unsigned>(m_ibounds.size()));
m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep));
} else {
auto& found_bound = m_ibounds[e->get_data().m_value];
auto& found_bound = m_ibounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = implied_bound(v, j, true, is_strict, explain_dep);
TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
@ -177,12 +177,12 @@ private:
void add_upper_bound_monic(lpvar j, const mpq& bound_val, bool is_strict, std::function <u_dependency* (int*)> explain_bound) {
j = lp().column_to_reported_index(j);
auto *e = m_improved_upper_bounds.find_core(j);
if (!e) {
unsigned k;
if (!m_improved_upper_bounds.find(j, k)) {
m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_ibounds.size()));
m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound));
} else {
auto& found_bound = m_ibounds[e->get_data().m_value];
auto& found_bound = m_ibounds[k];
if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = implied_bound(bound_val, j, false, is_strict, explain_bound);
TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
@ -336,9 +336,9 @@ private:
if (!m_imp.bound_is_interesting(j, kind, v))
return;
if (is_low) {
auto *e = m_improved_lower_bounds.find_core(j);
if (e) {
auto& found_bound = m_ibounds[e->get_data().m_value];
unsigned k;
if (m_improved_lower_bounds.find(j, k)) {
auto& found_bound = m_ibounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
found_bound.m_bound = v;
found_bound.m_strict = strict;
@ -351,9 +351,9 @@ private:
TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
}
} else { // the upper bound case
auto *e = m_improved_upper_bounds.find_core(j);
if (e) {
auto& found_bound = m_ibounds[e->get_data().m_value];
unsigned k;
if (m_improved_upper_bounds.find(j, k)) {
auto& found_bound = m_ibounds[k];
if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
found_bound.m_bound = v;
found_bound.m_strict = strict;
@ -591,12 +591,12 @@ private:
lp_assert(y_sign == 1 || y_sign == -1);
auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg;
const auto& v = val(x);
auto * e = table.find_core(v);
if (!e) {
unsigned found_i;;
if (!table.find(v, found_i)) {
table.insert(v, i);
} else {
explanation ex;
unsigned found_i = e->get_data().m_value;
unsigned base_of_found = lp().get_base_column_in_row(found_i);
if (is_int(x) != is_int(base_of_found) || ival(x).y != ival(base_of_found).y)
continue;

48
src/math/lp/monomial_bounds.cpp
View file

@ -24,7 +24,6 @@ namespace nla {
}
}
bool monomial_bounds::is_too_big(mpq const& q) const {
return rational(q).bitsize() > 256;
}
@ -258,53 +257,6 @@ namespace nla {
}
}
void monomial_bounds::unit_propagate() {
for (lpvar v : c().m_monics_with_changed_bounds)
unit_propagate(c().emons()[v]);
c().m_monics_with_changed_bounds.clear();
}
void monomial_bounds::unit_propagate(monic const& m) {
m_propagated.reserve(m.var() + 1, false);
if (m_propagated[m.var()])
return;
lpvar non_fixed = null_lpvar, zero_var = null_lpvar;
if (!is_linear(m, zero_var, non_fixed))
return;
c().trail().push(set_bitvector_trail(m_propagated, m.var()));
if (zero_var != null_lpvar) {
new_lemma lemma(c(), "fixed-values");
lemma.explain_fixed(zero_var);
lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0);
}
else {
rational k = rational(1);
for (auto v : m)
if (v != non_fixed) {
k *= c().lra.get_column_value(v).x;
if (k.is_big()) return;
}
new_lemma lemma(c(), "fixed-values");
for (auto v : m)
if (v != non_fixed)
lemma.explain_fixed(v);
if (non_fixed != null_lpvar) {
lp::lar_term term;
term.add_var(m.var());
term.add_monomial(-k, non_fixed);
lemma += ineq(term, lp::lconstraint_kind::EQ, 0);
} else {
lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k);
}
}
}
// returns true iff (all variables are fixed,
// or all but one variable are fixed) and the bounds are not big,
// or at least one variable is fixed to zero.

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

@ -20,7 +20,6 @@ namespace nla {
void var2interval(lpvar v, scoped_dep_interval& i);
bool is_too_big(mpq const& q) const;
bool propagate_down(monic const& m, lpvar u);
bool propagate_value(dep_interval& range, lpvar v);
bool propagate_value(dep_interval& range, lpvar v, unsigned power);
void compute_product(unsigned start, monic const& m, scoped_dep_interval& i);
@ -32,12 +31,11 @@ namespace nla {
// monomial propagation
bool_vector m_propagated;
void unit_propagate(monic const& m);
bool is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed);
public:
monomial_bounds(core* core);
void propagate();
void unit_propagate();
};
}

11
src/math/lp/nla_core.cpp
View file

@ -1836,17 +1836,6 @@ bool core::improve_bounds() {
}
return bounds_improved;
}
void core::propagate(vector<lemma>& lemmas) {
// propagate linear monomials, those that have all, or all but one, variables fixed
lemmas.reset();
m_lemma_vec = &lemmas;
m_monomial_bounds.unit_propagate();
}
} // end of nla

4
src/math/lp/nla_solver.cpp
View file

@ -46,10 +46,6 @@ namespace nla {
return m_core->check(lits, lemmas);
}
void solver::propagate(vector<lemma>& lemmas) {
m_core->propagate(lemmas);
}
void solver::push(){
m_core->push();
}

14
src/smt/theory_lra.cpp
View file

@ -2159,20 +2159,6 @@ public:
return true;
}
void propagate_nla() {
if (!m_nla)
return;
m_nla->propagate(m_nla_lemma_vector);
if (lp().get_status() == lp::lp_status::INFEASIBLE) {
TRACE("arith", tout << "propagation conflict\n";);
get_infeasibility_explanation_and_set_conflict();
}
else {
for (nla::lemma const& l : m_nla_lemma_vector)
false_case_of_check_nla(l);
}
}
bool should_propagate() const {
return bound_prop_mode::BP_NONE != propagation_mode();
}