From bf79d93d519aad538e9e4b2171cda90cd547c87d Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 23 Aug 2019 11:01:17 -0700
Subject: [PATCH] limit the row length in horner's scheme

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.cpp     | 4 ++++
 src/math/lp/nla_params.pyg | 2 ++
 src/math/lp/nla_settings.h | 9 +++++++--
 src/smt/theory_lra.cpp     | 2 ++
 4 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 8e614f3e9..4f2ff2f33 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -40,6 +40,10 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
 template <typename T>
 bool horner::row_is_interesting(const T& row) const {
     TRACE("nla_solver_details", m_core->print_term(row, tout););
+    if (row.size() > m_core->m_settings.horner_row_length_limit()) {
+        TRACE("nla_solver_details", tout << "disregard\n";);
+        return false;
+    }
     SASSERT(row_has_monomial_to_refine(row));
     m_row_var_set.clear();
     for (const auto& p : row) {
diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg
index 23d42f826..859c600a8 100644
--- a/src/math/lp/nla_params.pyg
+++ b/src/math/lp/nla_params.pyg
@@ -4,6 +4,8 @@ def_module_params('nla',
                    ('order', BOOL, True, 'run order lemmas'),
                    ('tangents', BOOL, True, 'run tangent lemmas'),
                    ('horner', BOOL, True, 'run horner\'s heuristic'),
+                   ('horner_frequency', UINT, 4, 'horner\'s call frequency'),
+                   ('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value')
                           ))           
 
 
diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h
index c26d17e0c..b68f96542 100644
--- a/src/math/lp/nla_settings.h
+++ b/src/math/lp/nla_settings.h
@@ -26,11 +26,14 @@ class nla_settings {
     bool m_run_horner;
     // how often to call the horner heuristic
     unsigned m_horner_frequency;
+    unsigned m_horner_row_length_limit;
 public:
     nla_settings() : m_run_order(true),
                      m_run_tangents(true),
                      m_run_horner(true),
-                     m_horner_frequency(4) {}
+                     m_horner_frequency(4),
+                     m_horner_row_length_limit(10)
+    {}
     
     bool run_order() const { return m_run_order; }
     bool& run_order() { return m_run_order; }
@@ -42,6 +45,8 @@ public:
     bool& run_horner() { return m_run_horner; }    
 
     unsigned horner_frequency() const { return m_horner_frequency; }
-    unsigned& horner_frequency() { return m_horner_frequency; }    
+    unsigned& horner_frequency() { return m_horner_frequency; }
+    unsigned horner_row_length_limit() const { return m_horner_row_length_limit; }
+    unsigned& horner_row_length_limit() { return m_horner_row_length_limit; }    
 };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index e57b6d6f3..ce4e4cec5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -451,6 +451,8 @@ class theory_lra::imp {
             m_nla->get_core()->m_settings.run_order() = nla.order();
             m_nla->get_core()->m_settings.run_tangents() = nla.tangents();
             m_nla->get_core()->m_settings.run_horner() = nla.horner();
+            m_nla->get_core()->m_settings.horner_frequency() = nla.horner_frequency();
+            m_nla->get_core()->m_settings.horner_row_length_limit() = nla.horner_row_length_limit();            
         }
     }