try with missed bounds

Z3Prover · Dec 2, 2023 · 7eab26e · 7eab26e
1 parent 5c1e7f7
commit 7eab26e
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 0 deletions.
diff --git 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
@@ -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);