From c2062c9b3d7711efe5ef7bd40af3cb8fdf500866 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jul 2023 17:32:29 -0700 Subject: [PATCH] x Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 49 +++++++++++++++-------------------- src/math/lp/nla_intervals.cpp | 29 --------------------- src/math/lp/nla_intervals.h | 29 ++++++++++++++++++++- 3 files changed, 49 insertions(+), 58 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 4778caf89..504bfdb7f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -710,29 +710,28 @@ bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { #define IS_INT_EXPR_DEPTH_LIMIT 100 bool arith_recognizers::is_int_expr(expr const *e) const { - if (is_int(e)) return true; - if (is_uninterp(e)) return false; + if (is_int(e)) + return true; + if (is_uninterp(e)) + return false; ptr_buffer todo; todo.push_back(e); rational r; unsigned i = 0; while (!todo.empty()) { ++i; - if (i > IS_INT_EXPR_DEPTH_LIMIT) {return false;} + if (i > IS_INT_EXPR_DEPTH_LIMIT) + return false; e = todo.back(); todo.pop_back(); - if (is_to_real(e)) { - // pass - } - else if (is_numeral(e, r) && r.is_int()) { - // pass - } - else if (is_add(e) || is_mul(e)) { - todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - } - else { + if (is_to_real(e)) + ; // pass + else if (is_numeral(e, r) && r.is_int()) + ; // pass + else if (is_add(e) || is_mul(e)) + todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + else return false; - } } return true; } @@ -782,8 +781,8 @@ expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) { return mk_add_simplify(args.size(), args.data()); - } + expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { expr_ref result(m_manager); @@ -829,8 +828,6 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con return plugin().is_considered_uninterpreted(f); } - - func_decl* arith_util::mk_ipower0() { sort* s = mk_int(); sort* rs[2] = { s, s }; @@ -866,18 +863,14 @@ func_decl* arith_util::mk_mod0() { bool arith_util::is_bounded(expr* n) const { expr* x = nullptr, * y = nullptr; while (true) { - if (is_idiv(n, x, y) && is_numeral(y)) { + if (is_idiv(n, x, y) && is_numeral(y)) n = x; - } - else if (is_mod(n, x, y) && is_numeral(y)) { + else if (is_mod(n, x, y) && is_numeral(y)) return true; - } - else if (is_numeral(n)) { + else if (is_numeral(n)) return true; - } - else { + else return false; - } } } @@ -925,7 +918,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const { return true; } return false; - } while (false); + } + while (false); return false; } @@ -947,5 +941,4 @@ bool arith_util::is_underspecified(expr* e) const { } } return false; -} - +} \ No newline at end of file diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index f2352b128..011160cbf 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -246,35 +246,6 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { return out; } -template -void intervals::set_var_interval1(lpvar v, interval& b) { - TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";); - lp::constraint_index ci; - rational val; - bool is_strict; - if (ls().has_lower_bound(v, ci, val, is_strict)) { - m_dep_intervals.set_lower(b, val); - m_dep_intervals.set_lower_is_open(b, is_strict); - m_dep_intervals.set_lower_is_inf(b, false); - if (wd == e_with_deps::with_deps) b.m_lower_dep = mk_dep(ci); - } - else { - m_dep_intervals.set_lower_is_open(b, true); - m_dep_intervals.set_lower_is_inf(b, true); - if (wd == e_with_deps::with_deps) b.m_lower_dep = nullptr; - } - if (ls().has_upper_bound(v, ci, val, is_strict)) { - m_dep_intervals.set_upper(b, val); - m_dep_intervals.set_upper_is_open(b, is_strict); - m_dep_intervals.set_upper_is_inf(b, false); - if (wd == e_with_deps::with_deps) b.m_upper_dep = mk_dep(ci); - } - else { - m_dep_intervals.set_upper_is_open(b, true); - m_dep_intervals.set_upper_is_inf(b, true); - if (wd == e_with_deps::with_deps) b.m_upper_dep = nullptr; - } -} template diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 4db9aad7b..bb558776a 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -53,7 +53,34 @@ public: void set_var_interval(lpvar v, interval& b); template - void set_var_interval1(lpvar v, interval& b); + void set_var_interval1(lpvar v, interval& b) { + TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";); + lp::constraint_index ci; + rational val; + bool is_strict; + if (ls().has_lower_bound(v, ci, val, is_strict)) { + m_dep_intervals.set_lower(b, val); + m_dep_intervals.set_lower_is_open(b, is_strict); + m_dep_intervals.set_lower_is_inf(b, false); + if (wd == dep_intervals::with_deps_t::with_deps) b.m_lower_dep = mk_dep(ci); + } + else { + m_dep_intervals.set_lower_is_open(b, true); + m_dep_intervals.set_lower_is_inf(b, true); + if (wd == dep_intervals::with_deps_t::with_deps) b.m_lower_dep = nullptr; + } + if (ls().has_upper_bound(v, ci, val, is_strict)) { + m_dep_intervals.set_upper(b, val); + m_dep_intervals.set_upper_is_open(b, is_strict); + m_dep_intervals.set_upper_is_inf(b, false); + if (wd == dep_intervals::with_deps_t::with_deps) b.m_upper_dep = mk_dep(ci); + } + else { + m_dep_intervals.set_upper_is_open(b, true); + m_dep_intervals.set_upper_is_inf(b, true); + if (wd == dep_intervals::with_deps_t::with_deps) b.m_upper_dep = nullptr; + } + } template bool set_var_interval2(lpvar v, scoped_dep_interval& b) {