integrate factorization to Grobner

src/math/dd/dd_pdd.cpp

@@ -1311,7 +1311,7 @@ namespace dd {
             return m.mk_var(var())*h + l;
     }
 
-    std::pair<unsigned_vector, pdd> pdd::var_factors() {
+    std::pair<unsigned_vector, pdd> pdd::var_factors() const {
         if (is_val())
             return { unsigned_vector(), *this };
         unsigned v = var();

src/math/dd/dd_pdd.h

@@ -367,7 +367,7 @@ namespace dd {
         /**
          * \brief factor out variables
          */
-        std::pair<unsigned_vector, pdd> var_factors();
+        std::pair<unsigned_vector, pdd> var_factors() const;
 
         pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }

src/math/lp/nla_core.cpp

@@ -35,7 +35,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_grobner(this),
     m_emons(m_evars),
     m_use_nra_model(false),
-    m_nra(s, m_nra_lim, *this)
+    m_nra(s, m_nra_lim, *this) 
 {
     m_nlsat_delay = lp_settings().nlsat_delay();
 }
@@ -56,9 +56,8 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
 
 rational core::value(const lp::lar_term& r) const {
     rational ret(0);
-    for (lp::lar_term::ival t : r) {
+    for (lp::lar_term::ival t : r) 
         ret += t.coeff() * val(t.column());
-    }
     return ret;
 }
 
@@ -78,10 +77,9 @@ bool core::ineq_holds(const ineq& n) const {
 }
 
 bool core::lemma_holds(const lemma& l) const {
-    for(const ineq &i : l.ineqs()) {
+    for (const ineq &i : l.ineqs()) 
         if (ineq_holds(i))
             return true;
-    }
     return false;
 }
 
@@ -1498,14 +1496,17 @@ lbool core::check(vector<lemma>& l_vec) {
     init_search();
 
     lbool ret = l_undef;
+    bool run_grobner = need_run_grobner();
+    bool run_horner = need_run_horner();
+    bool run_bounded_nlsat = should_run_bounded_nlsat();
 
     if (l_vec.empty() && !done()) 
         m_monomial_bounds();
     
-    if (l_vec.empty() && !done() && need_run_horner()) 
+    if (l_vec.empty() && !done() && run_horner) 
         m_horner.horner_lemmas();
 
-    if (l_vec.empty() && !done() && need_run_grobner()) 
+    if (l_vec.empty() && !done() && run_grobner) 
         m_grobner();                
 
     if (l_vec.empty() && !done()) 
@@ -1514,9 +1515,16 @@ lbool core::check(vector<lemma>& l_vec) {
     if (l_vec.empty() && !done()) 
         m_basics.basic_lemma(false);
 
-    if (!conflict_found() && !done() && should_run_bounded_nlsat())
+#if 0
+    if (l_vec.empty() && !done() && !run_horner) 
+        m_horner.horner_lemmas();
+
+    if (l_vec.empty() && !done() && !run_grobner) 
+        m_grobner();                    
+#endif
+
+    if (!conflict_found() && !done() && run_bounded_nlsat)
         ret = bounded_nlsat();
-    
 
     if (l_vec.empty() && !done() && ret == l_undef) {
         std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };

src/math/lp/nla_grobner.cpp

@@ -45,7 +45,6 @@ namespace nla {
         if (is_conflicting())
             return;
 
-#if 0
         if (propagate_bounds())
             return;
 
@@ -54,7 +53,7 @@ namespace nla {
 
         if (propagate_factorization())
             return;
-#endif   
+
         if (quota > 1)
             quota--;
 
@@ -86,19 +85,19 @@ namespace nla {
     }
 
     bool grobner::propagate_bounds() {
-        unsigned bounds = 0;
+        unsigned changed = 0;
         for (auto eq : m_solver.equations()) 
-            if (propagate_bounds(*eq) && ++bounds >= m_solver.number_of_conflicts_to_report())
+            if (propagate_bounds(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
                 return true;
-        return bounds > 0;
+        return changed > 0;
     }
 
     bool grobner::propagate_eqs() {
-        unsigned fixed = 0;
+        unsigned changed = 0;
         for (auto eq : m_solver.equations())
-            if (propagate_fixed(*eq) && ++fixed >= m_solver.number_of_conflicts_to_report())
+            if (propagate_fixed(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
                 return true;
-        return fixed > 0;
+        return changed > 0;
     }
 
     bool grobner::propagate_factorization() {
@@ -152,23 +151,23 @@ namespace nla {
 
     bool grobner::propagate_factorization(const dd::solver::equation& eq) {
         dd::pdd const& p = eq.poly();
-        if (!p.is_val() && p.lo().is_zero() && !p.hi().is_val() && p.hi().is_linear()) {
-            //IF_VERBOSE(0, verbose_stream() << "factored " << p << "\n");
-            unsigned v = p.var();
-            auto q = p.hi();
-            new_lemma lemma(c(), "pdd-factored");
-            add_dependencies(lemma, eq);
-            term t;
-            while (!q.is_val()) {
-                t.add_monomial(q.hi().val(), q.var());
-                q = q.lo();
-            }
-            lemma |= ineq(v, llc::EQ, rational::zero());
-            lemma |= ineq(t, llc::EQ, -q.val());
-            //lemma.display(verbose_stream());
-            return true;
+        auto [vars, q] = p.var_factors();
+        if (vars.empty() || !q.is_linear())
+            return false;
+
+        // IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
+        new_lemma lemma(c(), "pdd-factored");
+        add_dependencies(lemma, eq);
+        term t;
+        while (!q.is_val()) {
+            t.add_monomial(q.hi().val(), q.var());
+            q = q.lo();
         }
-        return false;
+        for (auto v : vars) 
+            lemma |= ineq(v, llc::EQ, rational::zero());
+        lemma |= ineq(t, llc::EQ, -q.val());
+        //lemma.display(verbose_stream());
+        return true;
     }