clean m_nla_lemma_vector in nla_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Sep 25, 2023 · 26a9b77 · 26a9b77
1 parent 87a839c
commit 26a9b77
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 6 deletions.
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
@@ -2027,11 +2027,12 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
         }
     }
 
-    void core::init_bound_propagation() {
+    void core::init_bound_propagation(vector<nla::lemma>& lemma_vector) {
         m_implied_bounds.clear();
         m_improved_lower_bounds.reset();
         m_improved_upper_bounds.reset();
         m_column_types = &lra.get_column_types();
+        lemma_vector.clear();
     }
 
 }  // namespace nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
@@ -451,7 +451,7 @@ class core {
     void save_tableau();
     bool integrality_holds();
     void calculate_implied_bounds_for_monic(lp::lpvar v);
-    void init_bound_propagation();    
+    void init_bound_propagation(vector<nla::lemma> &);    
 };  // end of core
 
 struct pp_mon {

diff --git 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() {
-        m_core->init_bound_propagation();
+    void solver::init_bound_propagation(vector<nla::lemma>& nla_lemma_vector) {
+        m_core->init_bound_propagation(nla_lemma_vector);
     }
 
 }
diff --git 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();
+        void init_bound_propagation(vector<nla::lemma>&);
     };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -2201,7 +2201,7 @@ class theory_lra::imp {
     }
 
     void propagate_bounds_for_touched_monomials() {
-        m_nla->init_bound_propagation();
+        m_nla->init_bound_propagation(m_nla_lemma_vector);
         for (unsigned v : m_nla->monics_with_changed_bounds()) 
             m_nla->calculate_implied_bounds_for_monic(v);