From 8018e276437444e5b223c66e9a96b6fa90a855b1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 23 Feb 2019 08:09:30 -1000 Subject: [PATCH] use m_rm_table.to_refine() when applying tangent lemma Signed-off-by: Lev Nachmanson --- src/shell/main.cpp | 2 +- src/util/lp/nla_solver.cpp | 8 +++----- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 1718e7314..9a21435fb 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -301,7 +301,7 @@ static void parse_cmd_line_args(int argc, char ** argv) { int STD_CALL main(int argc, char ** argv) { -#ifdef DUMP_ARGS +#ifdef DUMP_ARGS_ std::cout << "args are: "; for (int i = 0; i < argc; i++) std::cout << argv[i] <<" "; diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 9c30a73a0..bcb70e3ec 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -2554,10 +2554,9 @@ struct solver::imp { } bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const rooted_mon*& rm_found){ - // todo : run on m_rm_table.to_refine() - for (const auto& rm : m_rm_table.vec()) { - if (check_monomial(m_monomials[rm.orig_index()])) - continue; + for (unsigned i: m_rm_table.to_refine()) { + const auto& rm = m_rm_table.vec()[i]; + SASSERT (!check_monomial(m_monomials[rm.orig_index()])); rm_found = &rm; if (find_bfc_on_monomial(rm, bf)) { j = m_monomials[rm.orig_index()].var(); @@ -2567,7 +2566,6 @@ struct solver::imp { print_bfc(bf, tout); tout << ", product = " << vvr(rm) << ", but should be =" << vvr(bf.m_x)*vvr(bf.m_y); tout << ", j == "; print_var(j, tout) << "\n";); - rm_found = &rm; return true; } }