diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 08ae6f249..2f2e524aa 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -58,40 +58,28 @@ namespace nla { auto const& upper = dep.upper(range); auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE; ++c().lra.settings().stats().m_nla_propagate_bounds; - if (c().params().arith_nl_internal_bounds()) { - auto* d = dep.get_upper_dep(range); - propagate_bound(v, cmp, upper, d); - } - else { - lp::explanation ex; - dep.get_upper_dep(range, ex); - if (is_too_big(upper)) - return false; - new_lemma lemma(c(), "propagate value - upper bound of range is below value"); - lemma &= ex; - lemma |= ineq(v, cmp, upper); - TRACE("nla_solver", dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";); - } + lp::explanation ex; + dep.get_upper_dep(range, ex); + if (is_too_big(upper)) + return false; + new_lemma lemma(c(), "propagate value - upper bound of range is below value"); + lemma &= ex; + lemma |= ineq(v, cmp, upper); + TRACE("nla_solver", dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";); propagated = true; } if (should_propagate_lower(range, v, 1)) { auto const& lower = dep.lower(range); auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE; ++c().lra.settings().stats().m_nla_propagate_bounds; - if (c().params().arith_nl_internal_bounds()) { - auto* d = dep.get_lower_dep(range); - propagate_bound(v, cmp, lower, d); - } - else { - lp::explanation ex; - dep.get_lower_dep(range, ex); - if (is_too_big(lower)) - return false; - new_lemma lemma(c(), "propagate value - lower bound of range is above value"); - lemma &= ex; - lemma |= ineq(v, cmp, lower); - TRACE("nla_solver", dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";); - } + lp::explanation ex; + dep.get_lower_dep(range, ex); + if (is_too_big(lower)) + return false; + new_lemma lemma(c(), "propagate value - lower bound of range is above value"); + lemma &= ex; + lemma |= ineq(v, cmp, lower); + TRACE("nla_solver", dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";); propagated = true; } return propagated; @@ -196,19 +184,11 @@ namespace nla { // v = -2, [-1,+1]^2 < v^2 -> add bound v >= -1 ++c().lra.settings().stats().m_nla_propagate_bounds; auto le = dep.upper_is_open(range) ? llc::LT : llc::LE; - if (c().params().arith_nl_internal_bounds()) { - auto* d = dep.get_upper_dep(range); - if (p % 2 == 0) - d = dep.mk_join(d, c().lra.get_column_upper_bound_witness(v)); - propagate_bound(v, le, r, d); - } - else { - new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value"); - lemma &= ex; - if (p % 2 == 0) - lemma.explain_existing_upper_bound(v); - lemma |= ineq(v, le, r); - } + new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value"); + lemma &= ex; + if (p % 2 == 0) + lemma.explain_existing_upper_bound(v); + lemma |= ineq(v, le, r); return true; } } @@ -227,19 +207,6 @@ namespace nla { ++c().lra.settings().stats().m_nla_propagate_bounds; auto ge = dep.lower_is_open(range) ? llc::GT : llc::GE; auto le = dep.lower_is_open(range) ? llc::LT : llc::LE; - if (c().params().arith_nl_internal_bounds()) { - if (rational(dep.lower(range)).is_neg() || p % 2 == 1) { - auto* d = dep.get_lower_dep(range); - propagate_bound(v, ge, r, d); - return true; - } - if (c().get_lower_bound(v) >= 0) { - auto* d = dep.get_lower_dep(range); - d = dep.mk_join(d, c().lra.get_column_lower_bound_witness(v)); - propagate_bound(v, ge, r, d); - return true; - } - } lp::explanation ex; dep.get_lower_dep(range, ex); new_lemma lemma(c(), "propagate value - root case - lower bound of range is above value"); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6d14e7cc6..9fcda7f64 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -83,7 +83,6 @@ def_module_params(module_name='smt', ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), - ('arith.nl.internal_bounds', BOOL, False, 'use internal bounds propagation'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index d1a6c6f11..9bc830dd1 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -39,7 +39,6 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials(); m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds(); m_nl_arith_cross_nested = p.arith_nl_cross_nested(); - m_nl_arith_internal_bounds = p.arith_nl_internal_bounds(); arith_rewriter_params ap(_p); m_arith_eq2ineq = ap.eq2ineq(); @@ -96,5 +95,4 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials); DISPLAY_PARAM(m_nl_arith_optimize_bounds); DISPLAY_PARAM(m_nl_arith_cross_nested); - DISPLAY_PARAM(m_nl_arith_internal_bounds); } diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index c84cca23b..f19544157 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -108,8 +108,6 @@ struct theory_arith_params { bool m_nl_arith_propagate_linear_monomials = true; bool m_nl_arith_optimize_bounds = true; bool m_nl_arith_cross_nested = true; - bool m_nl_arith_internal_bounds = false; - theory_arith_params(params_ref const & p = params_ref()) { updt_params(p);