add a config parameter to grobner

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

src/math/grobner/pdd_solver.cpp

@@ -70,11 +70,9 @@ namespace dd {
     }
 
 
+// some of the config fields are set, others are calculated
     void solver::set_thresholds() {
         IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
-        if (m_to_simplify.size() == 0)
-            return;
-        m_config.m_eqs_threshold = 10 * ceil(log(m_to_simplify.size()))*m_to_simplify.size();
         m_config.m_expr_size_limit = 0;
         m_config.m_expr_degree_limit = 0;
         for (equation* e: m_to_simplify) {
@@ -89,9 +87,9 @@ namespace dd {
                    verbose_stream() << "set m_config.m_expr_degree_limit to " <<  m_config.m_expr_degree_limit << "\n";
                    );
         m_config.m_max_steps = 700;
-        m_config.m_max_simplified = 7000;
+        m_config.m_max_simplified = 7000;        
-        
     }
+
     void solver::saturate() {
         simplify();
         init_saturate();

src/math/grobner/pdd_solver.h

@@ -55,6 +55,7 @@ public:
         unsigned m_max_simplified;
         unsigned m_random_seed;
         bool     m_enable_exlin;
+        unsigned m_eqs_growth;
         config() :
             m_eqs_threshold(UINT_MAX),
             m_expr_size_limit(UINT_MAX),

src/math/lp/nla_core.cpp

@@ -1425,18 +1425,21 @@ void core::run_pdd_grobner() {
     // configure grobner
     // TBD: move this code somewhere self-contained, and tune it.
     double tree_size = 100;
+    unsigned gr_eq_size = 0;
     for (auto* e : m_pdd_grobner.equations()) {
         tree_size = std::max(tree_size, e->poly().tree_size());
+        gr_eq_size ++;
     }
     tree_size *= 10;
     struct dd::solver::config cfg;
     cfg.m_expr_size_limit = (unsigned)tree_size;
-    cfg.m_eqs_threshold = m_pdd_grobner.equations().size()*5;
+    cfg.m_max_steps = gr_eq_size;
-    cfg.m_max_steps = m_pdd_grobner.equations().size();
+    cfg.m_eqs_threshold = m_nla_settings.grobner_eqs_growth() * ceil(log(gr_eq_size + 1)) * gr_eq_size;;
+
     m_pdd_grobner.set(cfg);
+    m_pdd_grobner.set_thresholds();
 
     m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
-    m_pdd_grobner.set_thresholds();
     m_pdd_grobner.saturate();
     bool conflict = false;
     for (auto eq : m_pdd_grobner.equations()) {

src/math/lp/nla_params.pyg

@@ -4,11 +4,11 @@ def_module_params('nla',
                    ('order', BOOL, True, 'run order lemmas'),
                    ('tangents', BOOL, True, 'run tangent lemmas'),
                    ('horner', BOOL, True, 'run horner\'s heuristic'),
-                   ('horner_subs_fixed', BOOL, True, 'substitute fixed variables by constants'),
+                   ('horner_subs_fixed', BOOL, False, 'substitute fixed variables by constants'),
                    ('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'),
                    ('grobner', BOOL, True, 'run grobner\'s basis heuristic'),
-                   ('grobner_eqs_threshold', UINT, 512, 'grobner\'s maximum number of equalities'),
+                   ('grobner_eqs_growth', UINT, 10, 'grobner\'s maximum number of equalities'),
                    ('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants')
                           ))           
 

src/math/lp/nla_settings.h

@@ -29,9 +29,10 @@ class nla_settings {
     unsigned m_horner_row_length_limit;
     bool m_horner_subs_fixed;
     // grobner fields
-    bool m_run_grobner;
+    bool     m_run_grobner;
     unsigned m_grobner_row_length_limit;
-    bool m_grobner_subs_fixed;
+    bool     m_grobner_subs_fixed;
+    unsigned m_grobner_eqs_growth;
 public:
     nla_settings() : m_run_order(true),
                      m_run_tangents(true),
@@ -43,7 +44,8 @@ public:
                      m_grobner_row_length_limit(50),
                      m_grobner_subs_fixed(false)
     {}
-    
+    unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;}
+    unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;}
     bool run_order() const { return m_run_order; }
     bool& run_order() { return m_run_order; }
 

src/smt/theory_lra.cpp

@@ -456,6 +456,8 @@ class theory_lra::imp {
             m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit();
             m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner();
             m_nla->get_core()->m_nla_settings.grobner_subs_fixed() = nla.grobner_subs_fixed();
+            m_nla->get_core()->m_nla_settings.grobner_eqs_growth() =  nla.grobner_eqs_growth();
+            
         }
     }