add option to propagation quotients

for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.

src/math/lp/CMakeLists.txt

@@ -32,6 +32,7 @@ z3_add_component(lp
     nla_monotone_lemmas.cpp
     nla_order_lemmas.cpp
     nla_powers.cpp
+    nla_pp.cpp
     nla_solver.cpp
     nla_tangent_lemmas.cpp
     nla_throttle.cpp

src/math/lp/nla_core.cpp

@@ -52,6 +52,10 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
     };
 }
 
+void core::updt_params(params_ref const& p) {
+    m_grobner.updt_params(p);
+}
+    
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
     switch(cmp) {
     case llc::LE: return ls <= rs;
@@ -172,108 +176,6 @@ bool core::check_monic(const monic& m) const {
 }
     
 
-template <typename T>
-std::ostream& core::print_product(const T & m, std::ostream& out) const {
-    bool first = true;
-    for (lpvar v : m) {
-        if (!first) out << "*"; else first = false;
-        if (lp_settings().print_external_var_name())
-            out << "(" << lra.get_variable_name(v) << "=" << val(v) << ")";
-        else
-            out << "(j" << v << " = " << val(v) << ")";
-            
-    }
-    return out;
-}
-template <typename T>
-std::string core::product_indices_str(const T & m) const {
-    std::stringstream out;
-    bool first = true;
-    for (lpvar v : m) {
-        if (!first)
-            out << "*";
-        else
-            first = false;
-        out << "j" << v;;
-    }
-    return out.str();
-}
-
-std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
-    if (f.sign())
-        out << "- ";
-    if (f.is_var()) {
-        out << "VAR,  " << pp(f.var());
-    } else {
-        out << "MON, v" << m_emons[f.var()] << " = ";
-        print_product(m_emons[f.var()].rvars(), out);
-    }
-    out << "\n";
-    return out;
-}
-
-std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) const {
-    if (f.is_var()) {
-        out << pp(f.var());
-    } 
-    else {
-        out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]);
-    }
-    return out;
-}
-
-std::ostream& core::print_monic(const monic& m, std::ostream& out) const {
-    if (lp_settings().print_external_var_name())
-        out << "([" << m.var() << "] = " << lra.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
-    else 
-        out << "(j" << m.var() << " = " << val(m.var()) << " = ";
-    print_product(m.vars(), out) << ")\n";
-    return out;
-}
-
-
-std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const {
-    SASSERT(m.size() == 2);
-    out << "( x = " << pp(m[0]) << "* y = " << pp(m[1]) << ")";
-    return out;
-}
-
-std::ostream& core::print_monic_with_vars(lpvar v, std::ostream& out) const {
-    return print_monic_with_vars(m_emons[v], out);
-}
-template <typename T>
-std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
-    print_product(m, out) << "\n";
-    for (unsigned k = 0; k < m.size(); k++) {
-        print_var(m[k], out);
-    }
-    return out;
-}
-
-std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const {
-    out << "[" << pp(m.var()) << "]\n";
-    out << "vars:"; print_product_with_vars(m.vars(), out) << "\n";
-    if (m.vars() == m.rvars())
-        out << "same rvars, and m.rsign = " << m.rsign() << " of course\n";
-    else {
-        out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
-        out << "rsign:" << m.rsign() << "\n";
-    }
-    return out;
-}
-
-std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
-    out << "expl: ";
-    unsigned i = 0;
-    for (auto p : exp) {
-        out << "(" << p.ci() << ")";
-        lra.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.ci());
-        if (++i < exp.size())
-            out << "      ";
-    }
-    return out;
-}
-
 bool core::explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
     rational b(0); // the bound
     for (lp::lar_term::ival p : t) {
@@ -551,69 +453,6 @@ bool core::var_is_free(lpvar j) const {
     return lra.column_is_free(j);
 }
     
-std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
-    lra.print_term_as_indices(in.term(), out);
-    return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs();
-}
-
-std::ostream & core::print_var(lpvar j, std::ostream & out) const {
-    if (is_monic_var(j)) 
-        print_monic(m_emons[j], out);
-        
-    lra.print_column_info(j, out);
-    signed_var jr = m_evars.find(j);
-    out << "root=";
-    if (jr.sign()) {
-        out << "-";
-    }
-        
-    out << lra.get_variable_name(jr.var()) << "\n";
-    return out;
-}
-
-std::ostream & core::print_monics(std::ostream & out) const {
-    for (auto &m : m_emons) {
-        print_monic_with_vars(m, out);
-    }
-    return out;
-}    
-
-std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const {
-    std::unordered_set<lpvar> vars;
-    out << "ineqs: ";
-    if (l.ineqs().size() == 0) {
-        out << "conflict\n";
-    } else {
-        for (unsigned i = 0; i < l.ineqs().size(); i++) {
-            auto & in = l.ineqs()[i]; 
-            print_ineq(in, out);
-            if (i + 1 < l.ineqs().size()) out << " or ";
-            for (lp::lar_term::ival p: in.term())
-                vars.insert(p.j());
-        }
-        out << std::endl;
-        for (lpvar j : vars) {
-            print_var(j, out);
-        }
-        out << "\n";
-    }
-    return out;
-}
-    
-std::ostream & core::print_factorization(const factorization& f, std::ostream& out) const {
-    if (f.is_mon()){
-        out << "is_mon " << pp_mon(*this, f.mon());
-    } 
-    else {
-        for (unsigned k = 0; k < f.size(); k++ ) {
-            out << "(" << pp(f[k]) << ")";
-            if (k < f.size() - 1)
-                out << "*";
-        }
-    }
-    return out;
-}
-    
 bool core::find_canonical_monic_of_vars(const svector<lpvar>& vars, lpvar & i) const {
     monic const* sv = m_emons.find_canonical(vars);
     return sv && (i = sv->var(), true);
@@ -623,16 +462,6 @@ bool core::is_canonical_monic(lpvar j) const {
     return m_emons.is_canonical_monic(j);
 }
 
-
-void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const {
-    out << "rooted vars: ";
-    print_product(rm.rvars(), out) << "\n";
-    out << "mon:   " << pp_mon(*this, rm.var()) << "\n";
-    out << "value: " << var_val(rm) << "\n";
-    print_factorization(f, out << "fact: ") << "\n";
-}
-
-
 bool core::var_has_positive_lower_bound(lpvar j) const {
     return lra.column_has_lower_bound(j) && lra.get_lower_bound(j) > lp::zero_of_type<lp::impq>();
 }
@@ -771,35 +600,6 @@ bool core::vars_are_roots(const T& v) const {
 }
 
 
-
-template <typename T>
-void core::trace_print_rms(const T& p, std::ostream& out) {
-    out << "p = {\n";
-    for (auto j : p) {
-        out << "j = " << j << ", rm = " << m_emons[j] << "\n";
-    }
-    out << "}";
-}
-
-void core::print_monic_stats(const monic& m, std::ostream& out) {
-    if (m.size() == 2) return;
-    monic_coeff mc = canonize_monic(m);
-    for(unsigned i = 0; i < mc.vars().size(); i++){
-        if (abs(val(mc.vars()[i])) == rational(1)) {
-            auto vv = mc.vars();
-            vv.erase(vv.begin()+i);
-            monic const* sv = m_emons.find_canonical(vv);
-            if (!sv) {
-                out << "nf length" << vv.size() << "\n"; ;
-            }
-        }
-    }
-}
-    
-void core::print_stats(std::ostream& out) {
-}
-        
-
 void core::clear() {
     m_lemmas.clear();
     m_literals.clear();
@@ -1620,40 +1420,11 @@ bool core::no_lemmas_hold() const {
     return true;
 }
     
-    
 lbool core::test_check() {
     lra.set_status(lp::lp_status::OPTIMAL);
     return check();
 }
 
-std::ostream& core::print_terms(std::ostream& out) const {
-    for (const auto * t: lra.terms()) {
-        out << "term:"; print_term(*t, out) << std::endl;        
-        print_var(t->j(), out);
-    }
-    return out;
-}
-
-std::string core::var_str(lpvar j) const {
-    std::string result;
-    if (is_monic_var(j))
-        result += product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_");
-    else
-        result += std::string("j") + lp::T_to_string(j);
-    //    result += ":w" + lp::T_to_string(get_var_weight(j));
-    return result;
-}
-
-std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
-    return lp::print_linear_combination_customized(
-        t.coeffs_as_vector(),
-        [this](lpvar j) { return var_str(j); },
-        out);
-}
-
-
-
-
 std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e ) {
     auto ret = get_vars_of_expr(e);
     auto & ls = lra;
@@ -1676,12 +1447,10 @@ std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e
     return ret;
 }
 
-
 bool core::is_nl_var(lpvar j) const {
     return is_monic_var(j) || m_emons.is_used_in_monic(j);
 }
 
-
 unsigned core::get_var_weight(lpvar j) const {
     unsigned k = 0;
     switch (lra.get_column_type(j)) {

src/math/lp/nla_core.h

@@ -120,6 +120,8 @@ public:
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
 
+    void updt_params(params_ref const& p);
+    
     const indexed_uint_set&  active_var_set () const { return m_active_var_set;}
     bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
 
@@ -224,6 +226,8 @@ public:
     bool check_monic(const monic& m) const;
    
 
+    std::ostream & display_row(std::ostream& out, lp::row_strip<lp::mpq> const& row) const;
+    std::ostream & display(std::ostream& out);
     std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
     std::ostream & print_var(lpvar j, std::ostream & out) const;
     std::ostream & print_monics(std::ostream & out) const;    

src/math/lp/nla_grobner.cpp

@@ -11,6 +11,7 @@ Author:
 
 --*/
 #include "util/uint_set.h"
+#include "params/smt_params_helper.hpp"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
 #include "math/grobner/pdd_solver.h"
@@ -27,6 +28,11 @@ namespace nla {
         m_quota(m_core.params().arith_nl_gr_q())
     {}
 
+    void grobner::updt_params(params_ref const& p) {
+        smt_params_helper ph(p);
+        m_config.m_propagate_quotients = ph.arith_nl_grobner_propagate_quotients();
+    }
+
     lp::lp_settings& grobner::lp_settings() {
         return c().lp_settings();
     }
@@ -73,6 +79,10 @@ namespace nla {
             if (propagate_linear_equations())
                 return;
 
+            if (propagate_quotients())
+                return;
+            IF_VERBOSE(0, m_solver.display(verbose_stream() << "grobner\n"));
+            
         }
         catch (...) {
             
@@ -181,23 +191,12 @@ namespace nla {
 
         // IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
 
-        term t;
+        auto [t, offset] = linear_to_term(q);
-        rational lc(1);
-        auto ql = q;
-        while (!ql.is_val()) {
-            lc = lcm(lc, denominator(ql.hi().val()));
-            ql = ql.lo();
-        }
-        lc = lcm(denominator(ql.val()), lc);
 
-        while (!q.is_val()) {
-            t.add_monomial(lc*q.hi().val(), q.var());
-            q = q.lo();
-        }
         vector<ineq> ineqs;
         for (auto v : vars)
             ineqs.push_back(ineq(v, llc::EQ, rational::zero()));
-        ineqs.push_back(ineq(t, llc::EQ, -lc*q.val()));
+        ineqs.push_back(ineq(t, llc::EQ, -offset));
         for (auto const& i : ineqs)
             if (c().ineq_holds(i))
                 return false;
@@ -210,6 +209,151 @@ namespace nla {
         return true;
     }
 
+
+    std::pair<lp::lar_term, rational> grobner::linear_to_term(dd::pdd q) {
+        SASSERT(q.is_linear());
+        rational lc(1);
+        auto ql = q;
+        lp::lar_term t;
+        while (!ql.is_val()) {
+            lc = lcm(lc, denominator(ql.hi().val()));
+            ql = ql.lo();
+        }
+        lc = lcm(denominator(ql.val()), lc);
+
+        while (!q.is_val()) {
+            t.add_monomial(lc * q.hi().val(), q.var());
+            q = q.lo();
+        }
+        rational offset = lc * q.val();
+        return {t, offset};
+    }
+
+    bool grobner::propagate_quotients() {
+        if (!m_config.m_propagate_quotients)
+            return false;
+        unsigned changed = 0;
+        for (auto eq : m_solver.equations())
+            if (propagate_quotients(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
+                return true;
+        return changed > 0;
+    }
+
+    // factor each nl var at a time.
+    // x*y + z = 0
+    // x = 0 => z = 0
+    // y = 0 => z = 0
+    // z = 0 => x = 0 or y = 0
+    // z > 0 & x > 0 => x <= z
+    // z < 0 & x > 0 => x <= -z
+    // z > 0 & x < 0 => -x <= z
+    // z < 0 & x < 0 => -x <= -z
+    bool grobner::propagate_quotients(dd::solver::equation const& eq) {
+        dd::pdd const& p = eq.poly();
+        if (p.is_linear())
+            return false;
+        if (p.is_val())
+            return false;
+        auto v = p.var();
+        if (!c().var_is_int(v))
+            return false;
+        for (auto v : p.free_vars())
+            if (!c().var_is_int(v))
+                return false;
+        tracked_uint_set nl_vars;
+        for (auto const& m : p) {
+            if (m.vars.size() == 1)
+                continue;
+            for (auto j : m.vars)
+                nl_vars.insert(j);
+        }
+        dd::pdd_eval eval;
+        eval.var2val() = [&](unsigned j) { return val(j); };
+
+        for (auto v : nl_vars) {
+            auto& m = p.manager();
+            dd::pdd lc(m), r(m);
+            p.factor(v, 1, lc, r);
+            if (!r.is_linear())
+                continue;
+            auto v_value = val(v);
+            auto r_value = eval(r);
+            auto lc_value = eval(lc);
+            if (r_value == 0) {
+                if (v_value == 0)
+                    continue;
+                if (lc_value == 0)
+                    continue;
+                if (!lc.is_linear())
+                    continue;
+                auto [t, offset] = linear_to_term(lc);
+                auto [t2, offset2] = linear_to_term(r);
+                lemma_builder lemma(c(), "pdd-quotient");
+                add_dependencies(lemma, eq);
+                // v = 0 or lc = 0 or r != 0
+                lemma |= ineq(v, llc::EQ, rational::zero());
+                lemma |= ineq(t, llc::EQ, -offset);
+                lemma |= ineq(t2, llc::NE, -offset2);
+                return true;
+            }
+            // r_value != 0
+            if (v_value == 0) {
+                // v = 0 => r = 0
+                lemma_builder lemma(c(), "pdd-quotient");
+                add_dependencies(lemma, eq);
+                auto [t, offset] = linear_to_term(r);
+                lemma |= ineq(v, llc::NE, rational::zero());
+                lemma |= ineq(t, llc::EQ, -offset);
+                return true;
+            }
+            if (lc_value == 0) {
+                if (!lc.is_linear())
+                    continue;
+                // lc = 0 => r = 0
+                lemma_builder lemma(c(), "pdd-quotient");
+                add_dependencies(lemma, eq);
+                auto [t, offset] = linear_to_term(lc);
+                auto [t2, offset2] = linear_to_term(r);
+                lemma |= ineq(t, llc::NE, -offset);
+                lemma |= ineq(t2, llc::EQ, -offset2);
+                return true;            
+            }
+            if (divides(v_value, r_value))
+                continue;
+              
+            if (abs(v_value) > abs(r_value)) {
+                // v*c + r = 0 & v > 0 => r >= v or -r >= v or r = 0
+                lemma_builder lemma(c(), "pdd-quotient");
+                auto [t, offset] = linear_to_term(r);
+                add_dependencies(lemma, eq);
+                if (v_value > 0) {
+                    lemma |= ineq(v, llc::LE, rational::zero());
+                    lemma |= ineq(t, llc::EQ, -offset);
+                    t.add_monomial(rational(-1), v);
+                    lemma |= ineq(t, llc::GE, -offset);
+                    auto [t2, offset2] = linear_to_term(-r);
+                    t2.add_monomial(rational(-1), v);
+                    lemma |= ineq(t2, llc::GE, -offset2);
+                } 
+                else {
+                    // v*lc + r = 0 & v < 0 => r <= v or -r <= v or r = 0
+                    lemma |= ineq(v, llc::GE, rational::zero());
+                    lemma |= ineq(t, llc::EQ, -offset);
+                    t.add_monomial(rational(-1), v);
+                    lemma |= ineq(t, llc::LE, -offset);
+                    auto [t2, offset2] = linear_to_term(-r);
+                    t2.add_monomial(rational(-1), v);
+                    lemma |= ineq(t2, llc::LE, -offset2);
+                }
+                return true;
+            } 
+            // other division lemmas are possible.  
+            // also extend to non-linear r, non-linear lc         
+        }
+
+        return false;
+    }
+
     void grobner::explain(dd::solver::equation const& eq, lp::explanation& exp) {
         u_dependency_manager dm;
         vector<unsigned, false> lv;

src/math/lp/nla_grobner.h

@@ -19,6 +19,9 @@ namespace nla {
     class core;
 
     class grobner : common {
+        struct config {
+            bool m_propagate_quotients = false;
+        };
         dd::pdd_manager          m_pdd_manager;
         dd::solver               m_solver;
         lp::lar_solver&          lra;
@@ -27,6 +30,7 @@ namespace nla {
         unsigned                 m_delay_base = 0;
         unsigned                 m_delay = 0;
         bool                     m_add_all_eqs = false;
+        config                   m_config;
         std::unordered_map<unsigned_vector, lpvar, hash_svector> m_mon2var;
 
         lp::lp_settings& lp_settings();
@@ -44,6 +48,11 @@ namespace nla {
         bool propagate_linear_equations();
         bool propagate_linear_equations(dd::solver::equation const& eq);
 
+        bool propagate_quotients();
+        bool propagate_quotients(dd::solver::equation const& eq);
+
+        std::pair<lp::lar_term, rational> linear_to_term(dd::pdd q);
+        
         void add_dependencies(lemma_builder& lemma, dd::solver::equation const& eq);
         void explain(dd::solver::equation const& eq, lp::explanation& exp);
 
@@ -73,6 +82,7 @@ namespace nla {
     public:
         grobner(core *core);        
         void operator()();
+        void updt_params(params_ref const& p);
         dd::solver::equation_vector const& core_equations(bool all_eqs);
     }; 
 }

src/math/lp/nla_pp.cpp

@@ -0,0 +1,319 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+   nla_core.cpp
+
+Author:
+   Lev Nachmanson (levnach)
+   Nikolaj Bjorner (nbjorner)
+
+--*/
+
+#include "math/lp/nla_core.h"
+using namespace nla;
+
+template <typename T>
+std::ostream& core::print_product(const T& m, std::ostream& out) const {
+    bool first = true;
+    for (lpvar v : m) {
+        if (!first)
+            out << "*";
+        else
+            first = false;
+        if (lp_settings().print_external_var_name())
+            out << "(" << lra.get_variable_name(v) << "=" << val(v) << ")";
+        else
+            out << "(j" << v << " = " << val(v) << ")";
+    }
+    return out;
+}
+
+template <typename T>
+std::string core::product_indices_str(const T& m) const {
+    std::stringstream out;
+    bool first = true;
+    for (lpvar v : m) {
+        if (!first)
+            out << "*";
+        else
+            first = false;
+        out << "j" << v;
+        ;
+    }
+    return out.str();
+}
+
+std::ostream& core::print_factor(const factor& f, std::ostream& out) const {
+    if (f.sign())
+        out << "- ";
+    if (f.is_var()) {
+        out << "VAR,  " << pp(f.var());
+    } else {
+        out << "MON, v" << m_emons[f.var()] << " = ";
+        print_product(m_emons[f.var()].rvars(), out);
+    }
+    out << "\n";
+    return out;
+}
+
+std::ostream& core::print_factor_with_vars(const factor& f, std::ostream& out) const {
+    if (f.is_var()) {
+        out << pp(f.var());
+    } else {
+        out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]);
+    }
+    return out;
+}
+
+std::ostream& core::print_monic(const monic& m, std::ostream& out) const {
+    if (lp_settings().print_external_var_name())
+        out << "([" << m.var() << "] = " << lra.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
+    else
+        out << "(j" << m.var() << " = " << val(m.var()) << " = ";
+    print_product(m.vars(), out) << ")\n";
+    return out;
+}
+
+std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const {
+    SASSERT(m.size() == 2);
+    out << "( x = " << pp(m[0]) << "* y = " << pp(m[1]) << ")";
+    return out;
+}
+
+std::ostream& core::print_monic_with_vars(lpvar v, std::ostream& out) const {
+    return print_monic_with_vars(m_emons[v], out);
+}
+template <typename T>
+std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
+    print_product(m, out) << "\n";
+    for (unsigned k = 0; k < m.size(); k++) {
+        print_var(m[k], out);
+    }
+    return out;
+}
+
+std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const {
+    out << "[" << pp(m.var()) << "]\n";
+    out << "vars:";
+    print_product_with_vars(m.vars(), out) << "\n";
+    if (m.vars() == m.rvars())
+        out << "same rvars, and m.rsign = " << m.rsign() << " of course\n";
+    else {
+        out << "rvars:";
+        print_product_with_vars(m.rvars(), out) << "\n";
+        out << "rsign:" << m.rsign() << "\n";
+    }
+    return out;
+}
+
+std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
+    out << "expl: ";
+    unsigned i = 0;
+    for (auto p : exp) {
+        out << "(" << p.ci() << ")";
+        lra.constraints().display(out, [this](lpvar j) { return var_str(j); }, p.ci());
+        if (++i < exp.size())
+            out << "      ";
+    }
+    return out;
+}
+   
+std::ostream& core::print_ineq(const ineq& in, std::ostream& out) const {
+    lra.print_term_as_indices(in.term(), out);
+    return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs();
+}
+
+std::ostream& core::print_var(lpvar j, std::ostream& out) const {
+    if (is_monic_var(j))
+        print_monic(m_emons[j], out);
+
+    lra.print_column_info(j, out);
+    signed_var jr = m_evars.find(j);
+    out << "root=";
+    if (jr.sign()) {
+        out << "-";
+    }
+
+    out << lra.get_variable_name(jr.var()) << "\n";
+    return out;
+}
+
+std::ostream& core::print_monics(std::ostream& out) const {
+    for (auto& m : m_emons) {
+        print_monic_with_vars(m, out);
+    }
+    return out;
+}
+
+std::ostream& core::print_ineqs(const lemma& l, std::ostream& out) const {
+    std::unordered_set<lpvar> vars;
+    out << "ineqs: ";
+    if (l.ineqs().size() == 0) {
+        out << "conflict\n";
+    } else {
+        for (unsigned i = 0; i < l.ineqs().size(); i++) {
+            auto& in = l.ineqs()[i];
+            print_ineq(in, out);
+            if (i + 1 < l.ineqs().size()) out << " or ";
+            for (lp::lar_term::ival p : in.term())
+                vars.insert(p.j());
+        }
+        out << std::endl;
+        for (lpvar j : vars) {
+            print_var(j, out);
+        }
+        out << "\n";
+    }
+    return out;
+}
+
+std::ostream& core::print_factorization(const factorization& f, std::ostream& out) const {
+    if (f.is_mon()) {
+        out << "is_mon " << pp_mon(*this, f.mon());
+    } else {
+        for (unsigned k = 0; k < f.size(); k++) {
+            out << "(" << pp(f[k]) << ")";
+            if (k < f.size() - 1)
+                out << "*";
+        }
+    }
+    return out;
+}
+
+void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const {
+    out << "rooted vars: ";
+    print_product(rm.rvars(), out) << "\n";
+    out << "mon:   " << pp_mon(*this, rm.var()) << "\n";
+    out << "value: " << var_val(rm) << "\n";
+    print_factorization(f, out << "fact: ") << "\n";
+}
+
+template <typename T>
+void core::trace_print_rms(const T& p, std::ostream& out) {
+    out << "p = {\n";
+    for (auto j : p) {
+        out << "j = " << j << ", rm = " << m_emons[j] << "\n";
+    }
+    out << "}";
+}
+
+void core::print_monic_stats(const monic& m, std::ostream& out) {
+    if (m.size() == 2) return;
+    monic_coeff mc = canonize_monic(m);
+    for (unsigned i = 0; i < mc.vars().size(); i++) {
+        if (abs(val(mc.vars()[i])) == rational(1)) {
+            auto vv = mc.vars();
+            vv.erase(vv.begin() + i);
+            monic const* sv = m_emons.find_canonical(vv);
+            if (!sv) {
+                out << "nf length" << vv.size() << "\n";
+                ;
+            }
+        }
+    }
+}
+
+void core::print_stats(std::ostream& out) {
+}
+
+
+std::ostream& core::print_terms(std::ostream& out) const {
+    for (const auto* t : lra.terms()) {
+        out << "term:";
+        print_term(*t, out) << std::endl;
+        print_var(t->j(), out);
+    }
+    return out;
+}
+
+std::ostream& core::print_term(const lp::lar_term& t, std::ostream& out) const {
+    return lp::print_linear_combination_customized(
+        t.coeffs_as_vector(),
+        [this](lpvar j) { return var_str(j); },
+        out);
+}
+
+std::string core::var_str(lpvar j) const {
+    std::string result;
+    if (is_monic_var(j))
+        result += product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j]) ? "" : "_");
+    else
+        result += std::string("j") + lp::T_to_string(j);
+    //    result += ":w" + lp::T_to_string(get_var_weight(j));
+    return result;
+}
+
+std::ostream& core::display_row(std::ostream& out, lp::row_strip<lp::mpq> const& row) const {
+    auto display_coeff = [&](bool first, lp::mpq const& p) {
+        if (first && p == 1)
+            return;
+        if (first && p > 0)
+            out << p;
+        else if (p == 1)
+            out << " + ";
+        else if (p > 0)
+            out << " + " << p << " * ";
+        else if (p == -1)
+            out << " - ";
+        else if (first)
+            out << p << " * ";
+        else
+            out << " - " << -p << " * ";
+    };
+    auto display_var = [&](bool first, lp::mpq p, lp::lpvar v) {
+        if (is_monic_var(v)) {
+            for (auto w : m_emons[v].vars())
+                p *= m_evars.find(w).rsign();           
+        } 
+        else 
+            p *= m_evars.find(v).rsign();
+        
+        display_coeff(first, p);
+        if (is_monic_var(v)) {
+            bool first = true;
+            for (auto w : m_emons[v].vars())
+                out << (first ? (first = false, "") : " * ") << "j" << m_evars.find(w).var();
+        } 
+        else
+            out << "j" << m_evars.find(v).var();  
+    };
+
+    bool first = true;
+    for (auto const& ri : row) {
+        auto v = ri.var();
+        if (lra.column_is_fixed(v)) {
+            auto q = lra.get_column_value(v).x;
+            if (q == 0)
+                continue;
+            q = q * ri.coeff();
+            if (first)
+                out << q;
+            else if (q > 0)
+                out << " + " << q;
+            else if (q < 0)
+                out << " - " << -q;
+        }
+        else if (lra.column_has_term(v)) {
+            auto const& t = lra.get_term(v);
+            for (lp::lar_term::ival p : t) {
+                display_var(first, p.coeff() * ri.coeff(), p.j());
+                first = false;
+            }
+        } 
+        else {
+            display_var(first, ri.coeff(), ri.var());
+        }
+        first = false;
+    }
+    out << " = 0\n";
+    return out;
+}
+
+std::ostream& core::display(std::ostream& out) {
+    print_monics(out);
+    for (unsigned i = 0; i < lra.row_count(); ++i)
+        display_row(out, lra.get_row(i));
+    return out;
+}

src/math/lp/nla_solver.cpp

@@ -36,6 +36,10 @@ namespace nla {
         m_core->set_relevant(is_relevant);
     }
 
+    void solver::updt_params(params_ref const& p) {
+        m_core->updt_params(p);
+    }
+    
     bool solver::is_monic_var(lpvar v) const {
         return m_core->is_monic_var(v);
     }
@@ -71,7 +75,7 @@ namespace nla {
     }
     
     std::ostream& solver::display(std::ostream& out) const {    
-        m_core->print_monics(out);
+        m_core->display(out);
         if (use_nra_model()) 
             m_core->m_nra.display(out);
         return out;

src/math/lp/nla_solver.h

@@ -33,6 +33,7 @@ namespace nla {
         void add_bounded_division(lpvar q, lpvar x, lpvar y);
         void check_bounded_divisions();
         void set_relevant(std::function<bool(lpvar)>& is_relevant);
+        void updt_params(params_ref const& p);
         void push();
         void pop(unsigned scopes);
         bool need_check();

src/params/smt_params_helper.pyg

@@ -78,6 +78,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
                           ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
                           ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
+                          ('arith.nl.grobner_propagate_quotients', BOOL, False, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'),
                           ('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, 10, 'number of calls to final check before invoking bounded nlsat check'),

src/smt/theory_lra.cpp

@@ -269,6 +269,7 @@ class theory_lra::imp {
                 return ctx().is_relevant(th.get_enode(u));
             };
             m_nla->set_relevant(is_relevant);
+            m_nla->updt_params(ctx().get_params());
 
         }
     }
@@ -1286,23 +1287,24 @@ public:
         }
         else {
 
-            expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
             expr_ref mone(a.mk_int(-1), m);
-            expr_ref modmq(a.mk_sub(mod, abs_q), m);
             literal eqz = mk_literal(m.mk_eq(q, zero));
             literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
-            literal mod_lt_q = mk_literal(a.mk_le(modmq, mone));
+
             
             // q = 0 or p = (p mod q) + q * (p div q)
             // q = 0 or (p mod q) >= 0
-            // q = 0 or (p mod q) < abs(q)
+            // q >= 0 or (p mod q) + q <= -1
-            // q >= 0 or (p mod q) = (p mod -q)
+            // q <= 0 or (p mod q) - q <= -1            
+            // (p mod q) = (p mod -q)
 
             mk_axiom(eqz, eq);
             mk_axiom(eqz, mod_ge_0);
-            mk_axiom(eqz, mod_lt_q);
+            mk_axiom(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, a.mk_mul(mone, q)), mone)));
-            if (!a.is_uminus(q)) 
+            mk_axiom(mk_literal(a.mk_ge(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, q), mone)));
-                mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
+            expr* x = nullptr, * y = nullptr;
+            if (false && !(a.is_mul(q, x, y) && mone == x))
+                mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_mul(mone, q)))));
             
             m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
 
@@ -1658,6 +1660,9 @@ public:
                 return FC_CONTINUE;
             }
 
+            if (st == FC_GIVEUP)
+                IF_VERBOSE(0, display(verbose_stream()));
+
             if (!int_undef && !check_bv_terms())
                 return FC_CONTINUE;