From 896aba31f8b173a2108e7bf6fee778037acb4662 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 25 Sep 2023 14:20:24 -0700
Subject: [PATCH] move monomial propagation from theory_lra to nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/nla_solver.cpp | 6 ++++++
src/math/lp/nla_solver.h | 2 +-
src/smt/theory_lra.cpp | 11 +++--------
3 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index b16d14021..236b85d4f 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -108,4 +108,10 @@ namespace nla {
return m_core->lemmas();
}
+ void solver::propagate_bounds_for_touched_monomials() {
+ init_bound_propagation();
+ for (unsigned v : monics_with_changed_bounds())
+ calculate_implied_bounds_for_monic(v);
+ reset_monics_with_changed_bounds();
+ }
}
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index b4fba1f86..0448d840f 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -51,6 +51,6 @@ namespace nla {
void calculate_implied_bounds_for_monic(lp::lpvar v);
void init_bound_propagation();
vector<nla::lemma> const& lemmas() const;
-
+ void propagate_bounds_for_touched_monomials();
};
}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ce53b8f25..3b6a71b3d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2199,12 +2199,8 @@ public:
finish_bound_propagation();
}
- void propagate_bounds_for_touched_monomials() {
- m_nla->init_bound_propagation();
- for (unsigned v : m_nla->monics_with_changed_bounds())
- m_nla->calculate_implied_bounds_for_monic(v);
-
- m_nla->reset_monics_with_changed_bounds();
+ void propagate_bounds_for_monomials() {
+ m_nla->propagate_bounds_for_touched_monomials();
for (const auto & l : m_nla->lemmas())
false_case_of_check_nla(l);
}
@@ -2215,8 +2211,7 @@ public:
if (is_infeasible() || !should_propagate())
return;
- m_bp.init();
- propagate_bounds_for_touched_monomials();
+ propagate_bounds_for_monomials();
if (m.inc())
finish_bound_propagation();