optionally limit linearization

src/math/lp/nla_core.cpp

@@ -313,7 +313,7 @@ bool core::explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const {
         return false;
             
     m_evars.explain(signed_var(i, false), signed_var(j, sign), e);
-    TRACE(nla_solver, tout << "explained :"; lra.print_term_as_indices(t, tout););
+    TRACE(nla_solver, tout << "explained :"; lra.print_term_as_indices(t, tout) << "\n";);
     return true;            
 }
 
@@ -1342,7 +1342,7 @@ lbool core::check() {
     if (no_effect()) 
         m_basics.basic_lemma(true); 
 
-    if (no_effect()) 
+    if (no_effect() && m_params.arith_nl_linearize()) 
         m_basics.basic_lemma(false);
 
     if (no_effect()) 
@@ -1358,21 +1358,19 @@ lbool core::check() {
         if (!conflict_found() && params().arith_nl_nra() && num_calls % 50 == 0 && num_calls > 500)
             ret = bounded_nlsat();
 
-        // both tangent and monotonicity are expensive
+        if (m_params.arith_nl_linearize()) {
-        std::function<void(void)> check1 = [&]() { m_monotone.monotonicity_lemma();
+            // both tangent and monotonicity are expensive
-        };
+            std::function<void(void)> check1 = [&]() { m_monotone.monotonicity_lemma();
-        std::function<void(void)> check2 = [&]() { m_tangents.tangent_lemma();
+            };
-        };
+            std::function<void(void)> check2 = [&]() { m_tangents.tangent_lemma();
-
+            };
-
-        
-        std::pair<unsigned, std::function<void(void)>> checks[] = 
-            { 
-              { 2, check1 }, 
-              { 1, check2 }};
-        check_weighted(2, checks);
-
 
+            std::pair<unsigned, std::function<void(void)>> checks[] = 
+             { 
+               { 2, check1 }, 
+               { 1, check2 }};
+            check_weighted(2, checks);
+        }
     }
 
     if (no_effect() && params().arith_nl_nra()) {

src/math/lp/nla_core.h

@@ -187,11 +187,11 @@ public:
 
     // returns true if the combination of the Horner's schema and Grobner Basis should be called
     bool need_run_horner() const { 
-        return params().arith_nl_horner() && lp_settings().stats().m_nla_calls % params().arith_nl_horner_frequency() == 0; 
+        return params().arith_nl_linearize() && params().arith_nl_horner() && lp_settings().stats().m_nla_calls % params().arith_nl_horner_frequency() == 0; 
     }
 
     bool need_run_grobner() const {
-        return params().arith_nl_grobner();         
+        return params().arith_nl_linearize() && params().arith_nl_grobner();         
     }
 
     void set_active_vars_weights(nex_creator&);

src/math/lp/nla_order_lemmas.cpp

@@ -10,6 +10,7 @@
 #include "math/lp/nla_core.h"
 #include "math/lp/nla_common.h"
 #include "math/lp/factorization_factory_imp.h"
+#include "util/util.h"
 
 namespace nla {
 
@@ -42,7 +43,7 @@ void order::order_lemma_on_monic(const monic& m) {
             continue;
         if (ac.is_mon())
             order_lemma_on_binomial(ac.mon());
-        else
+        else if (c().params().arith_nl_linearize())
             order_lemma_on_factorization(m, ac);
         if (done())
             break;
@@ -81,6 +82,11 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int
     if (!c().var_is_int(x) && val(x).is_big())
         return;
     
+    auto vx = val(x);
+    // only allow limitted set of values of a
+    if (c().var_is_int(x) && !(vx.is_zero() || vx.is_one() || vx.is_minus_one() || vx.is_power_of_two()))
+        if (!c().m_params.arith_nl_linearize())
+            return;
 
     SASSERT(!_().mon_has_zero(xy.vars()));
     int sy = rat_sign(val(y));
@@ -219,7 +225,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
     TRACE(nla_solver,
           tout << "ab.size()=" << ab.size() << "\n";
           tout << "we should have mv =" << mv << " = " << fv << " = fv\n";
-          tout << "m = "; _().print_monic_with_vars(m, tout); tout << "\nab ="; _().print_factorization(ab, tout););
+          tout << "m = "; _().print_monic_with_vars(m, tout); tout << "\nab ="; _().print_factorization(ab, tout) << "\n";);
 
     if (mv != fv && !c().has_real(m)) {            
         bool gt = mv > fv;
@@ -239,7 +245,7 @@ void order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac,
     const factor c = ac[k];
     TRACE(nla_solver, tout << "c = "; _().print_factor_with_vars(c, tout); );
     if (c.is_var()) {
-        TRACE(nla_solver, tout << "var(c) = " << var(c););
+        TRACE(nla_solver, tout << "var(c) = " << var(c) << "\n";);
         for (monic const& bc : _().emons().get_use_list(c.var())) {
             if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) 
                 return;

src/params/smt_params_helper.pyg

@@ -89,6 +89,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
                           ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                           ('arith.nl.stellensatz', BOOL, False, 'enable stellensatz saturation'),
+                          ('arith.nl.linearize', BOOL, True, 'enable NL linearization'),
                           ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.epsilon', DOUBLE, 1.0, 'initial value of epsilon used for model generation of infinitesimals'),