add option to reduce pseudo-linear monomials

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

src/math/lp/nla_core.cpp

@@ -1308,6 +1308,10 @@ lbool core::check() {
     if (no_effect())
         m_monomial_bounds.propagate();
 
+    if (no_effect() && refine_pseudo_linear())
+        return l_false;
+       
+    
     {
         std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
         std::function<void(void)> check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); };
@@ -1519,6 +1523,54 @@ void core::simplify() {
 
 }
 
+bool core::is_pseudo_linear(monic const& m) const {
+    bool has_unbounded = false;
+    for (auto v : m.vars()) {
+        if (lra.column_is_bounded(v) && lra.var_is_int(v)) {
+            auto lb = lra.get_lower_bound(v);
+            auto ub = lra.get_upper_bound(v);
+            if (ub - lb <= rational(4))
+                continue;
+        }
+        if (has_unbounded)
+            return false;
+        has_unbounded = true;
+    }
+    return true;
+}
+
+bool core::refine_pseudo_linear() {
+    if (!params().arith_nl_reduce_pseudo_linear())
+        return false;
+    for (lpvar j : m_to_refine) {
+        if (is_pseudo_linear(m_emons[j])) {
+            refine_pseudo_linear(m_emons[j]);
+            return true;
+        }
+    }
+    return false;
+}
+
+void core::refine_pseudo_linear(monic const& m) {
+    lemma_builder lemma(*this, "nla-pseudo-linear");
+    lpvar nlvar = null_lpvar;
+    rational prod(1);
+    for (auto v : m.vars()) {
+        if (lra.column_is_bounded(v) && lra.var_is_int(v)) {
+            auto lb = lra.get_lower_bound(v);
+            auto ub = lra.get_upper_bound(v);
+            if (ub - lb <= rational(4)) {
+                lemma |= ineq(v, llc::NE, val(v));
+                prod *= val(v);
+                continue;
+            }
+        }
+        SASSERT(nlvar == null_lpvar);
+        nlvar = v;
+    }
+    lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0));
+    // lemma.display(verbose_stream() << "pseudo-linear lemma\n");
+}
 
 
 

src/math/lp/nla_core.h

@@ -111,7 +111,9 @@ class core {
     void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
     void add_bounds();
 
-
+    bool refine_pseudo_linear();
+    bool is_pseudo_linear(monic const& m) const;    
+    void refine_pseudo_linear(monic const& m);
 
 public:    
     // constructor

src/math/lp/nla_grobner.cpp

@@ -841,22 +841,6 @@ namespace nla {
             m_solver.add(p, dep);
     }
 
-    bool grobner::is_pseudo_linear(unsigned_vector const& vars) const {
-        bool has_unbounded = false;
-        for (auto v : vars) {
-            if (c().lra.column_is_bounded(v) && c().lra.var_is_int(v)) {
-                auto lb = c().lra.get_lower_bound(v);
-                auto ub = c().lra.get_upper_bound(v);
-                if (ub - lb <= rational(4))
-                    continue;                
-            }
-            if (has_unbounded)
-                return false;
-            has_unbounded = true;
-        }
-        return true;
-    }
-
     void grobner::add_fixed_monic(unsigned j) {
         u_dependency* dep = nullptr;
         dd::pdd r = m_pdd_manager.mk_val(rational(1));
@@ -882,7 +866,6 @@ namespace nla {
         TRACE(grobner, for (lpvar j : c().m_to_refine) print_monic(c().emons()[j], tout) << "\n";);
          
         for (lpvar j : c().m_to_refine)
-            if (!is_pseudo_linear(c().emons()[j].vars()))
             q.push_back(j);
     
         while (!q.empty()) {

src/math/lp/nla_grobner.h

@@ -79,7 +79,7 @@ namespace nla {
         void add_fixed_monic(unsigned j);
         bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
         void add_eq(dd::pdd& p, u_dependency* dep);        
-        bool is_pseudo_linear(unsigned_vector const& vars) const;
+        bool is_pseudo_linear(monic const& m) const;
         const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
         dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep);  
         dd::pdd pdd_expr(lp::lar_term const& t, u_dependency*& dep);

src/params/smt_params_helper.pyg

@@ -83,6 +83,7 @@ def_module_params(module_name='smt',
                           ('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, False, 'expand terms before computing grobner basis'),
+                          ('arith.nl.reduce_pseudo_linear', BOOL, False, 'create incremental linearization axioms for pseudo-linear monomials'),
                           ('arith.nl.delay', UINT, 10, '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'),