filter out empty lemmas from nla_solver on consumption

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/nla_solver.cpp

@@ -107,9 +107,9 @@ namespace nla {
     void solver::check_bounded_divisions() {
         m_core->check_bounded_divisions();
     }
-
+    //return only the non-empty lemmas
-    vector<nla::lemma> const& solver::lemmas() const {
+    solver::non_empty_lemmas_range solver::lemmas() const {
-        return m_core->lemmas();
+        return non_empty_lemmas_range(m_core->lemmas());
     }
     
     vector<nla::ineq> const& solver::literals() const {

src/math/lp/nla_solver.h

@@ -49,10 +49,68 @@ namespace nla {
         nlsat::anum const& am_value(lp::lpvar v) const;
         scoped_anum& tmp1();
         scoped_anum& tmp2();
-        vector<nla::lemma> const& lemmas() const;
         vector<nla::ineq> const& literals() const;
         vector<lp::fixed_equality> const& fixed_equalities() const;
         vector<lp::equality> const& equalities() const;
         bool should_check_feasible() const { return m_core->should_check_feasible(); }
+        
+        // Iterator class for filtering out empty lemmas
+        class non_empty_lemma_iterator {
+            vector<nla::lemma>::const_iterator current_;
+            vector<nla::lemma>::const_iterator end_;
+            
+            void advance_to_non_empty() {
+                while (current_ != end_ && current_->is_empty()) {
+                    std::cout << "skip\n";
+                    ++current_;
+                }
+            }
+            
+        public:
+            non_empty_lemma_iterator(vector<nla::lemma>::const_iterator start, 
+                                   vector<nla::lemma>::const_iterator end) 
+                : current_(start), end_(end) {
+                advance_to_non_empty();
+            }
+            
+            const nla::lemma& operator*() const { return *current_; }
+            const nla::lemma* operator->() const { return &*current_; }
+            
+            non_empty_lemma_iterator& operator++() {
+                ++current_;
+                advance_to_non_empty();
+                return *this;
+            }
+            
+            bool operator!=(const non_empty_lemma_iterator& other) const {
+                return current_ != other.current_;
+            }
+            
+            bool operator==(const non_empty_lemma_iterator& other) const {
+                return current_ == other.current_;
+            }
+        };
+        
+        // Helper class to provide range-based iteration over non-empty lemmas
+        class non_empty_lemmas_range {
+            const vector<nla::lemma>& lemmas_;
+        public:
+            non_empty_lemmas_range(const vector<nla::lemma>& lemmas) : lemmas_(lemmas) {}
+            
+            non_empty_lemma_iterator begin() const {
+                return non_empty_lemma_iterator(lemmas_.begin(), lemmas_.end());
+            }
+            
+            non_empty_lemma_iterator end() const {
+                return non_empty_lemma_iterator(lemmas_.end(), lemmas_.end());
+            }
+            
+            bool empty() const {
+                return begin() == end();
+            }
+        };
+        
+        non_empty_lemmas_range lemmas() const;
+        
     };
 }

src/smt/theory_lra.cpp

@@ -178,6 +178,9 @@ class theory_lra::imp {
     // integer arithmetic
     scoped_ptr<lp::int_solver> m_lia;
 
+    // temporary lemma storage
+    nla::lemma m_lemma;
+
 
     struct var_value_eq {
         imp & m_th;
@@ -1962,8 +1965,6 @@ public:
         return FC_DONE;
     }
 
-    nla::lemma m_lemma;
-
     literal mk_literal(nla::ineq const& ineq) {
         bool is_lower = true, pos = true, is_eq = false;
         switch (ineq.cmp()) {
@@ -2010,6 +2011,7 @@ public:
         m_lemma = l; //todo avoid the copy
         m_explanation = l.expl();
         literal_vector core;
+        SASSERT(!m_lemma.is_empty());
         for (auto const& ineq : m_lemma.ineqs()) {
             auto lit = mk_literal(ineq);
             core.push_back(~lit);