fix a bug in nla_intervals - add explanations when getting intervals …

…from a term Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Feb 29, 2020 · caa118c · caa118c
1 parent 4685317
commit caa118c
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 3 deletions.
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
@@ -166,7 +166,7 @@ rational core::product_value(const unsigned_vector & m) const {
 bool core::check_monic(const monic& m) const {    
     SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int());
     bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); 
-    CTRACE("nla_solver", !ret, print_monic(m, tout) << '\n';);
+    CTRACE("nla_solver_check_monic", !ret, print_monic(m, tout) << '\n';);
     return ret;
 }
 

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
@@ -77,7 +77,14 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
         return false;
     }
     auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
-    TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
+    TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout);
+          tout << ", expressions vars = \n";
+          for(lpvar j: m_core->get_vars_of_expr_with_opening_terms(n)) {
+              m_core->print_var(j, tout);
+          }
+          tout << "\n";
+          );
+
     std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
                                                          m_core->add_empty_lemma();
                                                          m_core->current_expl().add(e);
@@ -268,14 +275,20 @@ bool intervals::interval_from_term(const nex& e, interval& i) {
     lp::explanation exp;
     if (m_core->explain_by_equiv(norm_t, exp)) {
         set_zero_interval(i);
+        if (wd == e_with_deps::with_deps) {
+            for (auto p : exp) {
+                i.m_lower_dep = mk_join(i.m_lower_dep, mk_leaf(p.second));
+            }
+            i.m_upper_dep = i.m_lower_dep;
+        }
         TRACE("nla_intervals", tout << "explain_by_equiv\n";);
         return true;
     }
     lpvar j = find_term_column(norm_t, a);
     if (j + 1 == 0)
         return false;
 
-    set_var_interval<e_with_deps::without_deps>(j, i);
+    set_var_interval<wd>(j, i);
     interval bi;
     m_dep_intervals.mul<wd>(a, i, bi);
     m_dep_intervals.add(b, bi);