cache some fields in horner scheme and limit the number of reported cross nested forms

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

src/math/lp/cross_nested.h

@@ -43,6 +43,7 @@ class cross_nested {
     std::unordered_map<lpvar, unsigned>   m_powers;
     ptr_vector<nex>                       m_allocated;
     ptr_vector<nex>                       m_b_split_vec;
+    int                                   m_reported;
 #ifdef Z3DEBUG
     nex* m_e_clone;
 #endif
@@ -54,7 +55,8 @@ public:
                  std::function<bool (unsigned)> var_is_fixed):
         m_call_on_result(call_on_result),
         m_var_is_fixed(var_is_fixed),
-        m_done(false)
+        m_done(false),
+        m_reported(0)
     {}
 
     
@@ -354,7 +356,7 @@ public:
         if (occurences.empty()) {
             if(front.empty()) {
                 TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
-                m_done = m_call_on_result(m_e);
+                m_done = m_call_on_result(m_e) || ++m_reported > 100;
 // #ifdef Z3DEBUG
 //                 nex *ce = clone(m_e);
 //                 TRACE("nla_cn", tout << "ce = " << *ce <<  "\n";);
@@ -391,7 +393,7 @@ public:
             return;
         TRACE("nla_cn", tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";);
         if (front.empty()) {
-            m_done = m_call_on_result(m_e);
+            m_done = m_call_on_result(m_e) || ++m_reported > 100;
             return;
         }
         auto n = pop_front(front);

src/math/lp/horner.cpp

@@ -41,31 +41,27 @@ template <typename T>
 bool horner::row_is_interesting(const T& row) const {
     TRACE("nla_solver_details", m_core->print_term(row, tout););
     SASSERT(row_has_monomial_to_refine(row));
-    std::unordered_set<lpvar> seen;
+    m_row_var_set.clear();
     for (const auto& p : row) {
         lpvar j = p.var();
         if (!c().is_monomial_var(j))
             continue;
         auto & m = c().emons()[j];
         
-        std::unordered_set<lpvar> local_vars;
+        for (lpvar k : m.vars()) {
-        for (lpvar k : m.vars()) { // have to do it to ignore the powers
+            if (m_row_var_set.contains(k))
-            local_vars.insert(k);
-        }
-        for (lpvar k : local_vars) {
-            auto it = seen.find(k);
-            if (it == seen.end())
-                seen.insert(k);
-            else
                 return true;
         }
+        for (lpvar k : m.vars()) {
+            m_row_var_set.insert(k);
+        }
     }
     return false;
 }
 
-bool horner::lemmas_on_expr(nex_sum* e, cross_nested& cn) {
+bool horner::lemmas_on_expr(cross_nested& cn) {
-    TRACE("nla_horner", tout << "e = " << e << "\n";);
+    TRACE("nla_horner", tout << "m_row_sum = " << m_row_sum << "\n";);
-    cn.run(e);
+    cn.run(&m_row_sum);
     return cn.done();
 }
 
@@ -86,8 +82,8 @@ bool horner::lemmas_on_row(const T& row) {
         );
 
     SASSERT (row_is_interesting(row));
-    nex_sum* e = create_sum_from_row(row, cn);
+    create_sum_from_row(row, cn);
-    return lemmas_on_expr(e, cn);
+    return lemmas_on_expr(cn);
 }
 
 void horner::horner_lemmas() {
@@ -103,6 +99,7 @@ void horner::horner_lemmas() {
         for (auto & s : matrix.m_columns[j])
             rows_to_check.insert(s.var());
     }
+    m_row_var_set.resize(c().m_lar_solver.number_of_vars());
     svector<unsigned> rows;
     for (unsigned i : rows_to_check) {
         if (row_is_interesting(matrix.m_rows[i]))
@@ -147,18 +144,17 @@ nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const {
 }
 
 
-template <typename T> nex_sum* horner::create_sum_from_row(const T& row, cross_nested& cn) {
+template <typename T> void horner::create_sum_from_row(const T& row, cross_nested& cn) {
     TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
     SASSERT(row.size() > 1);
-    nex_sum *e = cn.mk_sum();
+    m_row_sum.children().clear();
     for (const auto &p : row) {
         if (p.coeff().is_one())
-            e->add_child(nexvar(p.var(), cn));
+            m_row_sum.add_child(nexvar(p.var(), cn));
         else {           
-            e->add_child(nexvar(p.coeff(), p.var(), cn));
+            m_row_sum.add_child(nexvar(p.coeff(), p.var(), cn));
         }
     }
-    return e;
 }
 
 

src/math/lp/horner.h

@@ -23,13 +23,16 @@
 #include "math/lp/nla_intervals.h"
 #include "math/lp/nex.h"
 #include "math/lp/cross_nested.h"
+#include "math/lp/int_set.h"
 
 namespace nla {
 class core;
 
 
 class horner : common {
-    intervals m_intervals;
+    intervals             m_intervals;
+    nex_sum               m_row_sum;
+    mutable lp::int_set   m_row_var_set;
 public:
     typedef intervals::interval interv;
     horner(core *core);
@@ -38,7 +41,7 @@ public:
     bool lemmas_on_row(const T&);
     template <typename T>  bool row_is_interesting(const T&) const;
     template <typename T>
-    nex_sum* create_sum_from_row(const T&, cross_nested&);
+    void create_sum_from_row(const T&, cross_nested&);
     intervals::interval interval_of_expr(const nex* e);
     
     nex* nexvar(lpvar j, cross_nested& cn) const;
@@ -48,7 +51,7 @@ public:
     intervals::interval interval_of_mul(const nex_mul*);
     void set_interval_for_scalar(intervals::interval&, const rational&);
     void set_var_interval(lpvar j, intervals::interval&) const;
-    bool lemmas_on_expr(nex_sum* , cross_nested&);
+    bool lemmas_on_expr(cross_nested&);
     
     template <typename T> // T has an iterator of (coeff(), var())
     bool row_has_monomial_to_refine(const T&) const;