Merge branch 'Z3Prover:master' into param-tuning

src/math/lp/nla_grobner.cpp

@@ -47,9 +47,22 @@ namespace nla {
         if (m_quota == 0)
             m_quota = c().params().arith_nl_gr_q();                    
 
+        bool const use_exp_delay = c().params().arith_nl_grobner_exp_delay();
+
         if (m_quota == 1) {
-            m_delay_base++;
-            m_delay = m_delay_base;
+            if (use_exp_delay) {
+                constexpr unsigned delay_cap = 1000000;
+                if (m_delay_base == 0)
+                    m_delay_base = 1;
+                else if (m_delay_base < delay_cap) {
+                    m_delay_base *= 2;
+                    if (m_delay_base > delay_cap)
+                        m_delay_base = delay_cap;
+                }
+                m_delay = m_delay_base;
+            }
+            else
+                m_delay = ++m_delay_base;
             m_quota = c().params().arith_nl_gr_q();
         }
 

src/nlsat/nlsat_explain.cpp

@@ -44,6 +44,7 @@ namespace nlsat {
         bool                    m_full_dimensional;
         bool                    m_minimize_cores;
         bool                    m_factor;
+        bool                    m_add_all_coeffs;
         bool                    m_signed_project;
         bool                    m_cell_sample;
 
@@ -154,6 +155,7 @@ namespace nlsat {
             m_simplify_cores   = false;
             m_full_dimensional = false;
             m_minimize_cores   = false;
+            m_add_all_coeffs   = true;
             m_signed_project   = false;
         }
 
@@ -622,6 +624,8 @@ namespace nlsat {
 //"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott
             
         bool is_square_free(polynomial_ref_vector &ps, var x) {
+            if (m_add_all_coeffs)
+                return false;
             polynomial_ref p(m_pm);
             polynomial_ref lc_poly(m_pm);
             polynomial_ref disc_poly(m_pm); 
@@ -2135,6 +2139,10 @@ namespace nlsat {
         m_imp->m_factor = f;
     }
 
+    void explain::set_add_all_coeffs(bool f) {
+        m_imp->m_add_all_coeffs = f;
+    }
+
     void explain::set_signed_project(bool f) {
         m_imp->m_signed_project = f;
     }
@@ -2185,4 +2193,3 @@ void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
     std::cout << std::endl;
 }
 #endif
-

src/nlsat/nlsat_explain.h

@@ -44,6 +44,7 @@ namespace nlsat {
         void set_full_dimensional(bool f);
         void set_minimize_cores(bool f);
         void set_factor(bool f);
+        void set_add_all_coeffs(bool f);
         void set_signed_project(bool f);
 
         /**
@@ -109,4 +110,3 @@ namespace nlsat {
     };
 
 };
-

src/nlsat/nlsat_params.pyg

@@ -19,5 +19,6 @@ def_module_params('nlsat',
                           ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"),
                           ('seed', UINT, 0, "random seed."),
                           ('factor', BOOL, True, "factor polynomials produced during conflict resolution."),
+                          ('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."),
                           ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only")
                           ))         

src/nlsat/nlsat_solver.cpp

@@ -306,6 +306,7 @@ namespace nlsat {
             m_explain.set_simplify_cores(m_simplify_cores);
             m_explain.set_minimize_cores(min_cores);
             m_explain.set_factor(p.factor());
+            m_explain.set_add_all_coeffs(p.add_all_coeffs());
             m_am.updt_params(p.p);
         }
 

src/params/smt_params_helper.pyg

@@ -80,6 +80,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                           ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'),
                           ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'),
+                          ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'),
                           ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
                           ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),   
                           ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
@@ -138,4 +139,3 @@ def_module_params(module_name='smt',
                           ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
                           ('qsat_use_qel', BOOL, True, 'Use QEL for lite quantifier elimination and model-based projection in QSAT')
                           ))
-