diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 079eccd74..904da26cd 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1913,26 +1913,81 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
}
}
- void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
- lp::impq bound_value;
- new_lemma lemma(*this, "propagate monic with non fixed");
- // using += to not assert thath the inequality does not hold
- lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
- lp::explanation exp;
- for (auto v : m_emons[monic_var].vars()) {
- if (v == non_fixed) continue;
- u_dependency* dep = lra.get_column_lower_bound_witness(v);
- for (auto ci : lra.flatten(dep)) {
- exp.push_back(ci);
- }
- dep = lra.get_column_upper_bound_witness(v);
- for (auto ci : lra.flatten(dep)) {
- exp.push_back(ci);
- }
- }
- lemma &= exp;
+void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
+{
+ lp::impq bound_value;
+ bool is_strict;
+ auto& lps = lra;
+
+ if (lower_bound_is_available(non_fixed)) {
+ bound_value = lra.column_lower_bound(non_fixed);
+ is_strict = !bound_value.y.is_zero();
+ auto lambda = [vars, non_fixed, &lps]() {
+ u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
+ for (auto v : vars)
+ if (v != non_fixed)
+ dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+ return dep;
+ };
+ if (k.is_pos())
+ add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+ else
+ add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
}
+ if (upper_bound_is_available(non_fixed)) {
+ bound_value = lra.column_upper_bound(non_fixed);
+ is_strict = !bound_value.y.is_zero();
+ auto lambda = [vars, non_fixed, &lps]() {
+ u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
+ for (auto v : vars)
+ if (v != non_fixed)
+ dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+ return dep;
+ };
+ if (k.is_neg())
+ add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+ else
+ add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+ }
+
+ if (lower_bound_is_available(monic_var)) {
+ auto lambda = [vars, monic_var, non_fixed, &lps]() {
+ u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
+ for (auto v : vars) {
+ if (v != non_fixed) {
+ dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+ }
+ }
+ return dep;
+ };
+ bound_value = lra.column_lower_bound(monic_var);
+ is_strict = !bound_value.y.is_zero();
+ if (k.is_pos())
+ add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+ else
+ add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+ }
+
+ if (upper_bound_is_available(monic_var)) {
+ bound_value = lra.column_upper_bound(monic_var);
+ is_strict = !bound_value.y.is_zero();
+ auto lambda = [vars, monic_var, non_fixed, &lps]() {
+ u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
+ for (auto v : vars) {
+ if (v != non_fixed) {
+ dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+ }
+ }
+ return dep;
+ };
+ if (k.is_neg())
+ add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+ else
+ add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+ }
+}
+
void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
{
auto* lps = &lra;
@@ -1976,14 +2031,12 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
}
}
- void core::init_bound_propagation(vector<lemma> & l_vec)
+ void core::init_bound_propagation()
{
m_implied_bounds.clear();
m_improved_lower_bounds.reset();
m_improved_upper_bounds.reset();
m_column_types = &lra.get_column_types();
- m_lemma_vec = &l_vec;
- m_lemma_vec->clear();
}
} // namespace nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 456709771..54c7e1df1 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -451,7 +451,7 @@ private:
void save_tableau();
bool integrality_holds();
void calculate_implied_bounds_for_monic(lp::lpvar v);
- void init_bound_propagation(vector<lemma>&);
+ void init_bound_propagation();
}; // end of core
struct pp_mon {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 08c1e1e62..3475a3509 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -100,8 +100,8 @@ namespace nla {
m_core->check_bounded_divisions(lemmas);
}
- void solver::init_bound_propagation(vector<lemma>& lemmas) {
- m_core->init_bound_propagation(lemmas);
+ void solver::init_bound_propagation() {
+ m_core->init_bound_propagation();
}
}
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index fa206ea40..a4de90320 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -49,6 +49,6 @@ namespace nla {
nlsat::anum const& am_value(lp::var_index v) const;
void collect_statistics(::statistics & st);
void calculate_implied_bounds_for_monic(lp::lpvar v);
- void init_bound_propagation(vector<lemma>&);
+ void init_bound_propagation();
};
}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index beec02d98..8ffeff3fb 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2205,7 +2205,7 @@ public:
}
void propagate_bounds_for_touched_monomials() {
- m_nla->init_bound_propagation(m_nla_lemma_vector);
+ m_nla->init_bound_propagation();
for (unsigned v : m_nla->monics_with_changed_bounds())
m_nla->calculate_implied_bounds_for_monic(v);
@@ -3891,7 +3891,6 @@ public:
IF_VERBOSE(1, verbose_stream() << enode_pp(n, ctx()) << " evaluates to " << r2 << " but arith solver has " << r1 << "\n");
}
}
-
};
theory_lra::theory_lra(context& ctx):