From ede4310b325800375fec7bc13b0489a425f255e0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 31 Oct 2019 20:14:43 -0700 Subject: [PATCH] port Grobner: still producing sat lemmas Signed-off-by: Lev Nachmanson --- src/math/lp/nex_creator.cpp | 2 +- src/math/lp/nla_common.cpp | 14 +++++++++++--- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 325928932..78c341434 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -671,7 +671,7 @@ void nex_creator::sort_join_sum(ptr_vector & children) { for (auto& p : map) { process_map_pair(p.first, p.second, children, allocated_nexs); } - if (common_scalar) { + if (common_scalar && !common_scalar->value().is_zero()) { children.push_back(common_scalar); } TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index fb12ed18e..ad64a09d4 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -125,9 +125,13 @@ unsigned common::random() { // creates a nex expression for the coeff and var, // replaces the fixed vars with scalars nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixed_as_scalars) { + SASSERT(!coeff.is_zero()); if (!c().is_monic_var(j)) { if (fixed_as_scalars && c().var_is_fixed(j)) { - return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x); + auto & b = c().m_lar_solver.get_lower_bound(j).x; + if (b.is_zero()) + return nullptr; + return cn.mk_scalar(coeff * b); } c().insert_to_active_var_set(j); return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); @@ -136,7 +140,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); for (lpvar k : m.vars()) { if (fixed_as_scalars && c().var_is_fixed(k)) { - e->coeff() *= c().m_lar_solver.get_lower_bound(k).x; + auto & b = c().m_lar_solver.get_lower_bound(j).x; + if (b.is_zero()) + return nullptr; + e->coeff() *= b; continue; } c().insert_to_active_var_set(k); @@ -157,7 +164,8 @@ template void common::create_sum_from_row(const T& row, sum.children().clear(); for (const auto &p : row) { nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars); - sum.add_child(e); + if (e) + sum.add_child(e); } TRACE("nla_horner", tout << "sum =" << sum << "\n";); }