add options to allow testing the effect of non-linear hammers

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/params/smt_params_helper.pyg

@@ -78,7 +78,10 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                           ('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.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),                       
+	                  ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
+			  ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
+			  ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
+			  ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),

src/smt/params/theory_arith_params.cpp

@@ -36,6 +36,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
     m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
     m_arith_auto_config_simplex = p.arith_auto_config_simplex();
+    m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
+    m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
+    m_nl_arith_cross_nested = p.arith_nl_cross_nested();
 
     arith_rewriter_params ap(_p);
     m_arith_eq2ineq = ap.eq2ineq();
@@ -89,4 +92,7 @@ void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_nl_arith_max_degree);
     DISPLAY_PARAM(m_nl_arith_branching);
     DISPLAY_PARAM(m_nl_arith_rounds);
+    DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials);
+    DISPLAY_PARAM(m_nl_arith_optimize_bounds);
+    DISPLAY_PARAM(m_nl_arith_cross_nested);
 }

src/smt/params/theory_arith_params.h

@@ -105,6 +105,9 @@ struct theory_arith_params {
     unsigned                m_nl_arith_max_degree = 6;
     bool                    m_nl_arith_branching = true;
     unsigned                m_nl_arith_rounds = 1024;
+    bool                    m_nl_arith_propagate_linear_monomials = true;
+    bool                    m_nl_arith_optimize_bounds = true;
+    bool                    m_nl_arith_cross_nested = true;
 
 
     theory_arith_params(params_ref const & p = params_ref()) {

src/smt/theory_arith_nl.h

@@ -902,6 +902,8 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_linear_monomials() {
+    if (!m_params.m_nl_arith_propagate_linear_monomials)
+        return false;
     if (!reflection_enabled())
         return false;
     TRACE("non_linear", tout << "propagating linear monomials...\n";);
@@ -2278,6 +2280,8 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
 */
 template<typename Ext>
 bool theory_arith<Ext>::max_min_nl_vars() {
+    if (!m_params.m_nl_arith_optimize_bounds)
+        return true;
     var_set             already_found;
     svector<theory_var> vars;
     for (theory_var v : m_nl_monomials) {
@@ -2360,7 +2364,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
             }
             break;
         case 1:
-            if (!is_cross_nested_consistent(vars))
+            if (m_params.m_nl_arith_cross_nested && !is_cross_nested_consistent(vars))
                 progress = true;
             break;
         case 2: