port Grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/nex.h

@@ -443,6 +443,34 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) {
 //     return less_than_nex(a, b, lt);
 // }
 
+inline rational get_nex_val(const nex* e, std::function<rational (unsigned)> var_val) {
+    switch (e->type()) {
+    case expr_type::SCALAR:
+        return to_scalar(e)->value();
+    case expr_type::SUM:
+        {
+            rational r(0);
+            for (auto c: *to_sum(e)) {
+                r += get_nex_val(c, var_val);
+            }
+            return r;
+        }
+    case expr_type::MUL:
+        {
+            const nex_mul * m = to_mul(e);
+            rational t = m->coeff();
+            for (auto& c: *m)
+                t *= get_nex_val(c.e(), var_val).expt(c.pow());
+            return t;
+        }
+    case expr_type::VAR:
+        return var_val(to_var(e)->var());
+    default:
+        TRACE("nla_cn_details", tout << e->type() << "\n";);
+        SASSERT(false);
+        return rational();
+    }
+}
 
 inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
         std::unordered_set<lpvar> r;

src/math/lp/nla_grobner.cpp

@@ -449,9 +449,6 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, e
 }
  
 void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
-    if(m_intervals->check_cross_nested_expr(target->exp(), target->dep())) {
-        register_report();
-    }
     if (new_target != target) {
         m_equations_to_unfreeze.push_back(target);
         to_remove.push_back(target);
@@ -470,6 +467,15 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
             to_remove.push_back(target);
         }
     }
+    if(m_intervals->check_cross_nested_expr(target->exp(), target->dep())) {
+        TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n";
+              tout << "vars = \n";
+              for (lpvar j : get_vars_of_expr(target->exp())) {
+                  c().print_var(j, tout);
+              }
+              tout << "\ntarget->exp() val = " << get_nex_val(target->exp(), [this](unsigned j) { return c().val(j); }) << "\n";);
+        register_report();       
+    }
 }
 
 bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {

src/math/lp/nla_intervals.cpp

@@ -5,6 +5,7 @@
 
 namespace nla {
 void intervals::set_var_interval_with_deps(lpvar v, interval& b) const {
+    TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";);
     lp::constraint_index ci;
     rational val;
     bool is_strict;
@@ -181,6 +182,7 @@ const nex* intervals::get_zero_interval_child(const nex_mul* e) const {
 
 
 intervals::interv intervals::interval_of_mul_with_deps(const nex_mul* e) {
+    TRACE("nla_intervals_details", tout << "e = " << *e << "\n";);
     const nex * zero_interval_child = get_zero_interval_child(e);
     if (zero_interval_child) {
         interv a = interval_of_expr_with_deps(zero_interval_child, 1);
@@ -189,7 +191,6 @@ intervals::interv intervals::interval_of_mul_with_deps(const nex_mul* e) {
         return a;   
     } 
         
-    SASSERT(e->is_mul());
     interv a;
     set_interval_for_scalar(a, e->coeff());
     TRACE("nla_intervals_details", tout << "a = "; display(tout, a); );
@@ -235,7 +236,7 @@ intervals::interv intervals::interval_of_mul(const nex_mul* e) {
         combine_deps(a, b, comb_rule, c);
         TRACE("nla_intervals_details", tout << "a "; display(tout, a););
         TRACE("nla_intervals_details", tout << "c "; display(tout, c););
-        set(a, c, 33); 
+        set_with_no_deps(a, c); 
         TRACE("nla_intervals_details", tout << "part mult "; display(tout, a););
     }
     TRACE("nla_intervals_details",  tout << "e=" << *e << "\n";
@@ -296,11 +297,9 @@ intervals::interv intervals::interval_of_sum_no_term(const nex_sum* e) {
         TRACE("nla_intervals_details_sum", tout <<  "es[" << k << "]= " << *es[k] << "\n";);
         interv b = interval_of_expr(es[k], 1);
         interv c;
-        interval_deps_combine_rule combine_rule;
         TRACE("nla_intervals_details_sum", tout << "a = "; display(tout, a) << "\nb = "; display(tout, b) << "\n";);
-        add(a, b, c, combine_rule);
-        combine_deps(a, b, combine_rule, c);
-        set(a, c, 22);
+        add(a, b, c);
+        set_with_no_deps(a, c);
         TRACE("nla_intervals_details_sum", tout << *es[k] << ", ";
               display(tout, a); tout << "\n";);
     }
@@ -434,7 +433,7 @@ bool intervals::interval_from_term(const nex* e, interv & i) const {
     interv bi;
     mul_no_deps(a, i, bi);
     add(b, bi);
-    set(i, bi, 44);
+    set_with_no_deps(i, bi);
     
     TRACE("nla_intervals",
           m_core->m_lar_solver.print_column_info(j, tout) << "\n";

src/math/lp/nla_intervals.h

@@ -212,7 +212,7 @@ public:
         a.m_upper_dep = b.m_upper_dep;
     }
 
-    void set(interval& a, const interval& b, int fooo) const {
+    void set_with_no_deps(interval& a, const interval& b) const {
         m_imanager.set(a, b);
     }