From 71c3a09f4a46f59f595c1434db10ec08cd9231c6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 30 Oct 2019 19:12:11 -0700 Subject: [PATCH] port Grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nex.h | 28 ++++++++++++++++++++++++++++ src/math/lp/nla_grobner.cpp | 12 +++++++++--- src/math/lp/nla_intervals.cpp | 13 ++++++------- src/math/lp/nla_intervals.h | 2 +- 4 files changed, 44 insertions(+), 11 deletions(-) diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 40b0823ca..0959f1d28 100644 --- a/src/math/lp/nex.h +++ b/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 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 get_vars_of_expr(const nex *e ) { std::unordered_set r; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 110733757..e303b0014 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/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& to_insert, equation* new_target, equation*& target, ptr_buffer& 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& 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) { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 73c3864c4..acce58f65 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/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"; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 71906e03a..c9e1d1d01 100644 --- a/src/math/lp/nla_intervals.h +++ b/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); }