only run grobner when horner fails, introduce concat instead copy

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

src/math/lp/horner.cpp

@@ -90,15 +90,15 @@ bool horner::lemmas_on_row(const T& row) {
     return lemmas_on_expr(cn, to_sum(e));
 }
 
-void horner::horner_lemmas() {
+bool horner::horner_lemmas() {
     if (!c().m_nla_settings.run_horner()) {
         TRACE("nla_solver", tout << "not generating horner lemmas\n";);
-        return;
+        return false;
     }
     c().lp_settings().stats().m_horner_calls++;
     const auto& matrix = c().m_lar_solver.A_r();
     // choose only rows that depend on m_to_refine variables
-    std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
+    std::set<unsigned> rows_to_check;
     for (lpvar j : c().m_to_refine) {
         for (auto & s : matrix.m_columns[j])
             rows_to_check.insert(s.var());
@@ -112,13 +112,15 @@ void horner::horner_lemmas() {
 
     unsigned r = c().random();
     unsigned sz = rows.size();
-    for (unsigned i = 0; i < sz; i++) {
+    bool conflict = false;
+    for (unsigned i = 0; i < sz && !conflict; i++) {
         m_row_index = rows[(i + r) % sz];
         if (lemmas_on_row(matrix.m_rows[m_row_index])) {
             c().lp_settings().stats().m_horner_conflicts++;
-            break;
+            conflict = true;
         }
     }
+    return conflict;
 }
 }
 

src/math/lp/horner.h

@@ -36,7 +36,7 @@ class horner : common {
 public:
     typedef intervals::interval interv;
     horner(core *core, intervals*);
-    void horner_lemmas();
+    bool horner_lemmas();
     template <typename T> // T has an iterator of (coeff(), var())
     bool lemmas_on_row(const T&);
     template <typename T>  bool row_is_interesting(const T&) const;

src/math/lp/nla_core.cpp

@@ -1280,10 +1280,11 @@ lbool core::incremental_linearization(bool constraint_derived) {
 // obtain the lemmas
 lbool core::inner_check(bool constraint_derived) {
     if (constraint_derived) {
-        if (need_to_call_horner())
+        if (need_to_call_algebraic_methods())
-            m_horner.horner_lemmas();
+            if (!(m_nla_settings.run_horner() && m_horner.horner_lemmas())) {
-        else if (need_to_call_grobner())
+                if (m_nla_settings.run_grobner())
-            m_grobner.grobner_lemmas();
+                    m_grobner.grobner_lemmas();
+            }
         if (done()) {
             return l_false;
         }

src/math/lp/nla_core.h

@@ -145,12 +145,12 @@ public:
     
     lpvar var(const factor& f) const { return f.var(); }
 
-    bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; }
+    // returns true if the combination of the Horner's schema and Grobner Basis should be called
-
+    bool need_to_call_algebraic_methods() const { 
-    bool need_to_call_grobner() const {
+	return
-        return m_nla_settings.run_grobner() &&
+            lp_settings().stats().m_nla_calls < 20 ||
-            lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0;
+            lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; 
-    }
+			}
 
     lbool incremental_linearization(bool);
     

src/math/lp/nla_grobner.cpp

@@ -247,7 +247,7 @@ grobner_core::equation* grobner_core::pick_next() {
         if (is_trivial(curr))
             to_delete.push_back(curr);
         else if (is_simpler(curr, r)) {
-            TRACE("grobner", tout << "preferring "; display_equation(tout, *curr););
+            TRACE("grobner", tout << "preferring " << *(curr->expr()) << "\n";);;
             r = curr;
         }
     }
@@ -255,7 +255,7 @@ grobner_core::equation* grobner_core::pick_next() {
         del_equation(e);
     if (r)
         m_to_simplify.erase(r);
-    TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else display_equation(tout, *r););
+    TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else tout << *r->expr() << "\n";);
     return r;
 }
 
@@ -279,11 +279,8 @@ void grobner_core::simplify_eq_by_using_to_superpose(equation& eq) {
         else { tout << "no simplification\n"; });
 }
 
-grobner_core::equation_set const& grobner_core::equations() {
+concat<grobner_core::equation_set, grobner_core::equation_set, grobner_core::equation*>  grobner_core::equations() {
-    m_all_eqs.reset();
+    return concat<grobner_core::equation_set, grobner_core::equation_set, grobner_core::equation*>(m_to_superpose, m_to_simplify);
-    for (auto e : m_to_simplify) m_all_eqs.insert(e);
-    for (auto e : m_to_superpose) m_all_eqs.insert(e);
-    return m_all_eqs;
 }
 
 void grobner_core::reset() {
@@ -778,14 +775,20 @@ void grobner_core::display_equations(std::ostream & out, equation_set const & v,
         display_equation(out, *e);
 }
 
+void grobner_core::display_equations_no_deps(std::ostream & out, equation_set const & v, char const * header) const {
+    out << header << "\n";
+    for (const equation* e : v) 
+        out << *(e->expr()) << "\n";
+}
+
 std::ostream& grobner_core::display_equation(std::ostream & out, const equation & eq) const {
     out << "expr = " << *eq.expr() << "\n";
     return display_dependency(out, eq.dep());
 }
 
 std::ostream& grobner_core::display(std::ostream& out) const {
-    display_equations(out, m_to_superpose, "m_to_superpose:");
+    display_equations_no_deps(out, m_to_superpose, "m_to_superpose:");
-    display_equations(out, m_to_simplify, "m_to_simplify:");
+    display_equations_no_deps(out, m_to_simplify, "m_to_simplify:");
     return out;
 }
 

src/math/lp/nla_grobner.h

@@ -36,6 +36,37 @@ struct grobner_stats {
     grobner_stats() { reset(); }
 };
 
+template <typename A, typename B, typename C>
+class concat {    
+    const A& m_a; // the first container
+    const B& m_b; // the second container    
+public:
+    class iterator {
+        const concat& m_c;
+        typename A::iterator m_a_it;
+        typename B::iterator m_b_it;
+    public:
+        iterator(const concat& c, bool begin):
+            m_c(c), m_a_it(begin? m_c.m_a.begin() : m_c.m_a.end()), m_b_it(begin? m_c.m_b.begin() : m_c.m_b.end()) {}
+        const C operator*() { return m_a_it != m_c.m_a.end() ? *m_a_it : *m_b_it; }
+        iterator& operator++() {
+            if (m_a_it != m_c.m_a.end())
+                m_a_it++;
+            else
+                m_b_it++;
+            return *this;
+        }
+        iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
+        bool operator==(iterator const& other) const { return m_a_it == other.m_a_it && m_b_it == other.m_b_it; }
+        bool operator!=(iterator const& other) const { return m_a_it != other.m_a_it || m_b_it != other.m_b_it; }
+    };
+
+    concat(const A& a, const B& b) : m_a(a), m_b(b) {}
+    iterator begin() { return iterator(*this, true); }
+    iterator end() { return iterator(*this, false); }
+
+};
+
 class grobner_core {
 public:
     struct params {
@@ -92,7 +123,6 @@ private:
     mutable common::ci_dependency_manager        m_dep_manager;
     nex_lt                                       m_lt;
     bool                                         m_changed_leading_term;
-    equation_set                                 m_all_eqs;
     params                                       m_params;
 
 public:
@@ -107,9 +137,10 @@ public:
     void reset();
     bool compute_basis_loop();
     void assert_eq_0(nex*, common::ci_dependency * dep);
-    equation_set const& equations();
+    concat<equation_set, equation_set, equation*> equations();
     common::ci_dependency_manager& dep() const { return m_dep_manager;  }
 
+    void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const;
     void display_equations(std::ostream& out, equation_set const& v, char const* header) const;
     std::ostream& display_equation(std::ostream& out, const equation& eq) const;
     std::ostream& display(std::ostream& out) const;

src/math/lp/nla_settings.h

@@ -67,8 +67,6 @@ public:
     bool run_grobner() const { return m_run_grobner; }
     bool& run_grobner() { return m_run_grobner; }    
 
-    unsigned grobner_frequency() const { return m_grobner_frequency; }
-    unsigned& grobner_frequency() { return m_grobner_frequency; }
     unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; }
     unsigned grobner_expr_size_limit() const { return m_grobner_expr_size_limit; }
 };

src/smt/theory_lra.cpp

@@ -453,7 +453,6 @@ class theory_lra::imp {
             m_nla->get_core()->m_nla_settings.run_horner() = nla.horner();
             m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency();
             m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit();
-            m_nla->get_core()->m_nla_settings.grobner_frequency() = nla.grobner_frequency();
             m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner();
             m_nla->get_core()->m_nla_settings.grobner_eqs_threshold() = nla.grobner_eqs_threshold();
         }