change internalize_mod to internalize_div to to handle real division

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

src/math/dd/pdd_interval.h

@@ -129,26 +129,35 @@ public:
             get_interval<w_dep::without_deps>(p.lo(), lo_interval);
             m_dep_intervals.sub(bound, lo_interval, hi_bound);
             m_dep_intervals.div(hi_bound, p.hi().val().to_mpq(), hi_bound);
+            m_dep_intervals.display(verbose_stream() << "hi bound ", hi_bound) << "\n";
             scoped_ptr_vector<scoped_dep_interval> var_intervals;
             scoped_dep_interval var_interval(m());
+            m_dep_intervals.display(verbose_stream() << "var interval ", var_interval) << "\n";
             m_var2intervals(p.var(), true, var_intervals);
             for (auto* vip : var_intervals) {
                 auto & vi = *vip;
-                if (!m_dep_intervals.lower_is_inf(vi) && !m_dep_intervals.lower_is_inf(hi_bound) && rational(m_dep_intervals.lower(vi)) > m_dep_intervals.lower(hi_bound)) {
+                m_dep_intervals.display(verbose_stream() << " interval ", vi) << "\n";
+                if (!m_dep_intervals.lower_is_inf(vi) && !m_dep_intervals.lower_is_inf(hi_bound) && rational(m_dep_intervals.lower(vi)) >= m_dep_intervals.lower(hi_bound)) {
                     if (m_dep_intervals.lower_is_inf(var_interval) || m_dep_intervals.lower(vi) > m_dep_intervals.lower(var_interval)) {
+                        verbose_stream() << "insert-lower\n";
                         m_dep_intervals.set_lower(var_interval, m_dep_intervals.lower(vi));
+                        m_dep_intervals.set_lower_is_inf(var_interval, false);
                         m_dep_intervals.set_lower_dep(var_interval, m_dep_intervals.lower_dep(vi));                        
                     }
                 }
-                if (!m_dep_intervals.upper_is_inf(vi) && !m_dep_intervals.upper_is_inf(hi_bound) && m_dep_intervals.upper(hi_bound) > m_dep_intervals.upper(vi)) {
+                if (!m_dep_intervals.upper_is_inf(vi) && !m_dep_intervals.upper_is_inf(hi_bound) && m_dep_intervals.upper(hi_bound) >= m_dep_intervals.upper(vi)) {
                     if (m_dep_intervals.upper_is_inf(var_interval) || m_dep_intervals.upper(var_interval) > m_dep_intervals.upper(vi)) {
+                        verbose_stream() << "insert-upper\n";
                         m_dep_intervals.set_upper(var_interval, m_dep_intervals.upper(vi));
+                        m_dep_intervals.set_upper_is_inf(var_interval, false);
                         m_dep_intervals.set_upper_dep(var_interval, m_dep_intervals.upper_dep(vi));                        
                     }
                 }
             }
+            m_dep_intervals.display(verbose_stream() << "var interval after ", var_interval) << "\n";
             m_dep_intervals.mul(var_interval, p.hi().val().to_mpq(), hi_interval);
             m_dep_intervals.sub(bound, hi_interval, lo_bound);
+            m_dep_intervals.display(verbose_stream() << "lo bound ", lo_bound) << "\n";
             explain(p.lo(), lo_bound, lo_interval);
         }
         m_dep_intervals.add<dep_intervals::with_deps>(lo_interval, hi_interval, ret);

src/math/lp/nla_grobner.cpp

@@ -274,9 +274,17 @@ namespace nla {
         if (di.upper(i) >= mx)
             return false;
 
-        eval.var2intervals() = [this](lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
+        eval.var2intervals() = [&](lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
             verbose_stream() << "get-intervals\n";
-            // var2intervals(j, deps, intervals);
+            scoped_ptr<scoped_dep_interval> a = alloc(scoped_dep_interval, di);
+            scoped_ptr<scoped_dep_interval> b = alloc(scoped_dep_interval, di);
+            if (deps) c().m_intervals.set_var_interval1<dd::w_dep::with_deps>(j, *a);
+            else c().m_intervals.set_var_interval1<dd::w_dep::without_deps>(j, *a);
+            intervals.push_back(a.detach());
+            if (deps && c().m_intervals.set_var_interval2<dd::w_dep::with_deps>(j, *b))
+                intervals.push_back(b.detach());
+            if (!deps && c().m_intervals.set_var_interval2<dd::w_dep::without_deps>(j, *b))
+                intervals.push_back(b.detach());
         };
         // TODO - relax bound dependencies to weakest that admit within interval -mx, mx.
         eval.explain(lo, i, i_wd);

src/math/lp/nla_grobner.h

@@ -8,6 +8,7 @@
   --*/
 #pragma once
 
+#include "util/scoped_ptr_vector.h"
 #include "math/lp/nla_common.h"
 #include "math/lp/nla_intervals.h"
 #include "math/lp/nex.h"
@@ -48,7 +49,7 @@ namespace nla {
         
         void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);
 
-        void var2intervals(lpvar j, bool deps, vector<scoped_dep_interval>& intervals);
+        void var2intervals(lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals);
 
         // setup
         void configure();

src/smt/theory_lra.cpp

@@ -451,6 +451,17 @@ class theory_lra::imp {
         return s;
     }
 
+    theory_var internalize_div(app* n) {
+        TRACE("arith", tout << "internalizing...\n" << mk_pp(n, m) << "\n";);
+        rational r(1);
+        theory_var s = mk_binary_op(n);
+        if (!a.is_numeral(n->get_arg(1), r) || r.is_zero())
+            found_underspecified(n);
+        if (!ctx().relevancy())
+            mk_div_axiom(n->get_arg(0), n->get_arg(1));
+        return s;
+    }
+
     theory_var internalize_idiv(app * n) {
         rational r(1);
         theory_var s      = mk_binary_op(n);
@@ -552,7 +563,7 @@ class theory_lra::imp {
         else if (a.is_idiv(n))
             return internalize_idiv(n);
         else if (a.is_div(n))
-            return internalize_mod(n);
+            return internalize_div(n);
         else if (a.is_uminus(n)) 
             return internalize_uminus(n);
         else if (a.is_sub(n))