From 7eab26e3ef365cfab076dd13c23d9512dba16d08 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Dec 2023 10:48:35 -0800
Subject: [PATCH] try with missed bounds

---
 src/math/lp/nla_grobner.cpp | 40 +++++++++++++++++++++++++++++++++++++
 src/math/lp/nla_grobner.h   |  2 ++
 2 files changed, 42 insertions(+)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 92c02ab8036..a95aa766d2a 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -399,9 +399,49 @@ namespace nla {
         for (auto eq : m_solver.equations()) 
             if (propagate_linear_equations(*eq))
                 ++changed;
+#if 0
+        for (auto eq : m_solver.equations()) 
+            if (check_missed_bound(*eq))
+                return true;
+#endif
         return changed > 0;
     }
     
+    bool grobner::check_missed_bound(dd::solver::equation const& e) {
+        auto& di = c().m_intervals.get_dep_intervals();
+        auto set_var_interval = [&](lpvar j, scoped_dep_interval& a) {
+            c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
+        };
+        scoped_dep_interval i(di), t(di), s(di), u(di);
+        di.set_value(i, rational::zero());
+
+        for (auto const& [coeff, vars] : e.poly()) {
+            if (vars.empty())
+                di.add(coeff, i);
+            else {
+                di.set_value(t, rational::one());
+                for (auto v : vars) {
+                    set_var_interval(v, s);
+                    di.mul<dd::w_dep::with_deps>(coeff, s, s);
+                    di.add<dd::w_dep::with_deps>(t, s, t);
+                }
+                if (m_mon2var.find(vars) != m_mon2var.end()) {
+                    auto v = m_mon2var.find(vars)->second;
+                    set_var_interval(v, u);
+                    di.intersect<dd::w_dep::with_deps>(t, u, t);
+                }
+                di.add<dd::w_dep::with_deps>(i, t, i);
+            }
+        }
+        if (!di.separated_from_zero(i)) 
+            return false;
+        std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
+            new_lemma lemma(m_core, "pdd");
+            lemma &= e;
+        };
+        return di.check_interval_for_conflict_on_zero(i, e.dep(), f);
+    }
+    
     bool grobner::propagate_linear_equations(dd::solver::equation const& e) {
         if (equation_is_true(e))
             return false;
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index bf5ea8dcf24..e70b5473d41 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -47,6 +47,8 @@ namespace nla {
 
         bool propagate_linear_equations();
         bool propagate_linear_equations(dd::solver::equation const& eq);
+
+        bool check_missed_bound(dd::solver::equation const& eq);
         
         void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq);
         void explain(dd::solver::equation const& eq, lp::explanation& exp);