merge

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

src/math/lp/int_solver.cpp

@@ -172,7 +172,8 @@ namespace lp {
 
     lia_move int_solver::check(lp::explanation * e) {
         SASSERT(lra.ax_is_correct());
-        if (!has_inf_int()) return lia_move::sat;
+        if (!has_inf_int())
+            return lia_move::sat;
 
         m_t.clear();
         m_k.reset();
@@ -181,7 +182,8 @@ namespace lp {
         m_upper = false;
         lia_move r = lia_move::undef;
 
-        if (m_gcd.should_apply()) r = m_gcd();
+        if (m_gcd.should_apply())
+            r = m_gcd();
 
         check_return_helper pc(lra);
 
@@ -298,7 +300,6 @@ namespace lp {
         return m_number_of_calls % settings().m_int_find_cube_period == 0;
     }
 
-
     bool int_solver::should_gomory_cut() {
         return m_number_of_calls % settings().m_int_gomory_cut_period == 0;
     }

src/math/lp/lia_move.h

@@ -49,4 +49,8 @@ inline std::string lia_move_to_string(lia_move m) {
         };
         return "strange";
     }
+
+    inline std::ostream& operator<<(std::ostream& out, lia_move const& m) {
+        return out << lia_move_to_string(m);
+    }
 }

src/math/lp/monomial_bounds.cpp

@@ -58,10 +58,12 @@ 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 UNIT_PROPAGATE_BOUNDS
+            if (c().params().arith_nl_internal_bounds()) {
                 auto* d = dep.get_upper_dep(range);
-            c().lra.update_column_type_and_bound(v, cmp, upper, d);
+                TRACE("arith", tout << "upper " << cmp << " " << upper << "\n");
-#else
+                propagate_bound(v, cmp, upper, d);
+            }
+            else {
                 lp::explanation ex;
                 dep.get_upper_dep(range, ex);
                 if (is_too_big(upper))
@@ -70,17 +72,19 @@ namespace nla {
                 lemma &= ex;
                 lemma |= ineq(v, cmp, upper); 
                 TRACE("nla_solver", dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";);
-#endif
+            }
             return true;
         }
         else if (dep.is_above(range, val)) {
             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 UNIT_PROPAGATE_BOUNDS
+            if (c().params().arith_nl_internal_bounds()) {
                 auto* d = dep.get_lower_dep(range);
-            c().lra.update_column_type_and_bound(v, cmp, lower, d);            
+                propagate_bound(v, cmp, lower, d);
-#else
+                TRACE("arith", tout << v << " " << cmp << " " << lower << "\n");
+            }
+            else {
                 lp::explanation ex;
                 dep.get_lower_dep(range, ex);
                 if (is_too_big(lower))
@@ -89,7 +93,7 @@ namespace nla {
                 lemma &= ex;
                 lemma |= ineq(v, cmp, lower); 
                 TRACE("nla_solver", dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";);
-#endif
+            }
             return true;
         }
         else {
@@ -97,6 +101,28 @@ namespace nla {
         }
     }
 
+    /**
+     * Ensure that bounds are integral when the variable is integer.
+     */
+    void monomial_bounds::propagate_bound(lpvar v, lp::lconstraint_kind cmp, rational const& q, u_dependency* d) {
+        SASSERT(cmp != llc::EQ && cmp != llc::NE);
+        if (!c().var_is_int(v))
+            c().lra.update_column_type_and_bound(v, cmp, q, d);
+        else if (q.is_int()) {
+            if (cmp == llc::GT)
+                c().lra.update_column_type_and_bound(v, llc::GE, q + 1, d);
+            else if(cmp == llc::LT)
+                c().lra.update_column_type_and_bound(v, llc::LE, q - 1, d);
+            else
+                c().lra.update_column_type_and_bound(v, cmp, q, d);
+        }
+        else if (cmp == llc::GE || cmp == llc::GT) 
+            c().lra.update_column_type_and_bound(v, llc::GE, ceil(q), d);
+        else
+            c().lra.update_column_type_and_bound(v, llc::LE, floor(q), d);
+    }
+
+
     /**
      * val(v)^p should be in range.
      * if val(v)^p > upper(range) add 
@@ -129,28 +155,30 @@ namespace nla {
                 if ((p % 2 == 1) || val_v.is_pos()) {
                     ++c().lra.settings().stats().m_nla_propagate_bounds;
                     auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
-#if UNIT_PROPAGATE_BOUNDS
+                    if (c().params().arith_nl_internal_bounds()) {
-                    auto* d = dep.get_upper_dep();
+                        auto* d = dep.get_upper_dep(range);
-                    c().lra.update_column_type_and_bound(v, le, r, d);
+                        propagate_bound(v, le, r, d);
-#else
+                    }
+                    else {
                         new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
                         lemma &= ex;
                         lemma |= ineq(v, le, r);
-#endif
+                    }
                     return true;
                 }
                 if (p % 2 == 0 && val_v.is_neg()) {
                     ++c().lra.settings().stats().m_nla_propagate_bounds;
                     SASSERT(!r.is_neg());
                     auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
-#if UNIT_PROPAGATE_BOUNDS
+                    if (c().params().arith_nl_internal_bounds()) {
-                    auto* d = dep.get_upper_dep();
+                        auto* d = dep.get_upper_dep(range);
-                    c().lra.update_column_type_and_bound(v, ge, -r, d);
+                        propagate_bound(v, ge, -r, d);
-#else
+                    }
+                    else {
                         new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value");
                         lemma &= ex;
                         lemma |= ineq(v, ge, -r);
-#endif
+                    }
                     return true;
                 }
             }
@@ -306,10 +334,11 @@ namespace nla {
         if (m.is_propagated())
             return;
         lpvar w, fixed_to_zero;
-        if (!is_linear(m, w, fixed_to_zero)) {
+
-#if UNIT_PROPAGATE_BOUNDS
+        if (!is_linear(m)) {
+            if (c().params().arith_nl_internal_bounds()) {
                 propagate(m);
-#endif            
+            }  
             return;
         }
 

src/math/lp/monomial_bounds.h

@@ -17,6 +17,7 @@ namespace nla {
     class monomial_bounds : common {
         dep_intervals& dep;
 
+        void propagate_bound(lpvar v, lp::lconstraint_kind cmp, rational const& q, u_dependency* d);
         void var2interval(lpvar v, scoped_dep_interval& i);
         bool is_too_big(mpq const& q) const;
         bool propagate_down(monic const& m, lpvar u);

src/smt/params/smt_params_helper.pyg

@@ -83,6 +83,7 @@ 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'),

src/smt/params/theory_arith_params.cpp

@@ -39,6 +39,7 @@ 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();
@@ -95,4 +96,5 @@ 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);
 }

src/smt/params/theory_arith_params.h

@@ -108,6 +108,7 @@ 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()) {

src/smt/theory_lra.cpp

@@ -2113,7 +2113,6 @@ public:
     bool propagate_core() {
         m_model_is_initialized = false;
         flush_bound_axioms();
-        // disabled in master:
         propagate_nla(); 
         if (ctx().inconsistent())
             return true;
@@ -3175,8 +3174,7 @@ public:
                   ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n";              
               for (auto e : m_eqs) 
                   tout << pp(e.first, m) << " = " << pp(e.second, m) << "\n";
-              tout << " ==> ";
+              tout << " ==> " << pp(x, m) << " = " << pp(y, m) << "\n";
-              tout << pp(x, m) << " = " << pp(y, m) << "\n";
               );
         
         std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
@@ -3291,11 +3289,11 @@ public:
               tout << "lemma scope: " << ctx().get_scope_level();
               for (auto const& p : m_params) tout << " " << p;
               tout << "\n";
-              display_evidence(tout, m_explanation);
+              display_evidence(tout, m_explanation););
-              display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto ev : m_explanation) 
             set_evidence(ev.ci(), m_core, m_eqs);
 
+        SASSERT(!m_core.empty() || !m_eqs.empty());
         
         // SASSERT(validate_conflict(m_core, m_eqs));
         if (is_conflict) {