x

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<const expr> 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;
-}
-
+}

src/math/lp/nla_intervals.cpp

@@ -246,35 +246,6 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
     return out;
 }
 
-template <e_with_deps wd>
-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 <e_with_deps wd>

src/math/lp/nla_intervals.h

@@ -53,7 +53,34 @@ public:
     void set_var_interval(lpvar v, interval& b);
 
     template <dep_intervals::with_deps_t wd>
-    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 <dep_intervals::with_deps_t wd>
     bool set_var_interval2(lpvar v, scoped_dep_interval& b) {