add optional feature to bound search within ranges

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

src/smt/params/smt_params_helper.pyg

@@ -75,6 +75,7 @@ def_module_params(module_name='smt',
                           ('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
                           ('arith.rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info'),
                           ('arith.min', BOOL, False, 'minimize cost'),
+                          ('arith.bounded_expansion', BOOL, False, 'box variables used in branch and bound into bound assumptions'),
                           ('arith.print_stats', BOOL, False, 'print statistic'),
                           ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
                           ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),

src/smt/params/theory_arith_params.cpp

@@ -38,6 +38,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_reflect = p.arith_reflect();
     m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
     m_arith_auto_config_simplex = p.arith_auto_config_simplex();
+    m_arith_bounded_expansion = p.arith_bounded_expansion();
 
     arith_rewriter_params ap(_p);
     m_arith_eq2ineq = ap.eq2ineq();
@@ -78,6 +79,7 @@ void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_arith_adaptive_gcd);
     DISPLAY_PARAM(m_arith_propagation_threshold);
     DISPLAY_PARAM(m_arith_pivot_strategy);
+    DISPLAY_PARAM(m_arith_bounded_expansion);
     DISPLAY_PARAM(m_arith_add_binary_bounds);
     DISPLAY_PARAM(m_arith_propagation_strategy);
     DISPLAY_PARAM(m_arith_eq_bounds);

src/smt/params/theory_arith_params.h

@@ -82,6 +82,8 @@ struct theory_arith_params {
     bool                    m_arith_adaptive_gcd;
     unsigned                m_arith_propagation_threshold;
 
+    bool                    m_arith_bounded_expansion;
+
     arith_pivot_strategy    m_arith_pivot_strategy;
 
     // used in diff-logic
@@ -139,6 +141,7 @@ struct theory_arith_params {
         m_arith_eager_gcd(false),
         m_arith_adaptive_gcd(false),
         m_arith_propagation_threshold(UINT_MAX),
+        m_arith_bounded_expansion(false),
         m_arith_pivot_strategy(ARITH_PIVOT_SMALLEST),
         m_arith_add_binary_bounds(false),
         m_arith_propagation_strategy(ARITH_PROP_PROPORTIONAL),

src/smt/theory_lra.cpp

@@ -932,7 +932,11 @@ public:
         m_solver(nullptr),
         m_resource_limit(*this),
         m_farkas("farkas"),
-        m_bp(*this)
+        m_bp(*this),
+        m_bounded_range_idx(0),
+        m_bounded_range_lit(null_literal),
+        m_bound_predicates(m),
+        m_bound_predicate(m)
     {
     }
         
@@ -1769,7 +1773,13 @@ public:
     }
     // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
     app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
-        rational offset = k;
+        rational offset;
+        expr_ref t(m);
+        return mk_bound(term, k, lower_bound, offset, t);
+    }
+
+    app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound, rational& offset, expr_ref& t) {
+        offset = k;
         u_map<rational> coeffs;
         term2coeffs(term, coeffs);
         bool is_int = true;
@@ -1815,7 +1825,7 @@ public:
         //        tout << "offset: " << offset << " gcd: " << g << "\n";);
 
         app_ref atom(m);
-        app_ref t = coeffs2app(coeffs, rational::zero(), is_int);
+        t = coeffs2app(coeffs, rational::zero(), is_int);
         if (lower_bound) {
             atom = a.mk_ge(t, a.mk_numeral(offset, is_int));
         }
@@ -2056,7 +2066,9 @@ public:
             app_ref b(m);
             bool u = m_lia->is_upper();
             auto const & k = m_lia->get_offset();
-            b = mk_bound(m_lia->get_term(), k, !u);
+            rational offset;
+            expr_ref t(m);
+            b = mk_bound(m_lia->get_term(), k, !u, offset, t);
             if (m.has_trace_stream()) {
                 app_ref body(m);
                 body = m.mk_or(b, m.mk_not(b));
@@ -2071,6 +2083,7 @@ public:
             // SAT core assigns a value to
             lia_check = l_false;
             ++m_stats.m_branch;
+            add_variable_bound(t, offset);
             break;
         }
         case lp::lia_move::cut: {
@@ -3874,6 +3887,100 @@ public:
         st.update("arith-assume-eqs", m_stats.m_assume_eqs);
         st.update("arith-branch", m_stats.m_branch);
     }        
+
+    /*
+     * Facility to put a small box around integer variables used in branch and bounds.
+     */
+
+    struct bound_info {
+        rational m_offset;
+        unsigned m_range;
+        bound_info() {}
+        bound_info(rational const& o, unsigned r):m_offset(o), m_range(r) {}
+    };
+    unsigned                  m_bounded_range_idx;  // current size of bounded range.
+    literal                   m_bounded_range_lit;  // current bounded range literal
+    expr_ref_vector           m_bound_predicates; // predicates used for bounds
+    expr_ref                  m_bound_predicate;
+    obj_map<expr, expr*>      m_predicate2term;
+    obj_map<expr, bound_info> m_term2bound_info;
+
+    bool use_bounded_expansion() const { 
+        return ctx().get_fparams().m_arith_bounded_expansion; 
+    }
+
+    unsigned init_range() const { return 5; }
+    unsigned max_range() const { return 20; }
+    
+    void add_theory_assumptions(expr_ref_vector& assumptions) {
+        if (!use_bounded_expansion())
+            return;
+        ctx().push_trail(value_trail<context, literal>(m_bounded_range_lit));
+        m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort());
+        m_bounded_range_lit = mk_literal(m_bound_predicate);
+        // add max-unfolding literal
+        // add variable bounds
+        assumptions.push_back(m_bound_predicate);
+        for (auto const& kv : m_term2bound_info) {
+            bound_info const& bi = kv.m_value;
+            expr* t = kv.m_key;
+            expr_ref hi(a.mk_le(t, a.mk_int(bi.m_offset + bi.m_range)), m);
+            expr_ref lo(a.mk_ge(t, a.mk_int(bi.m_offset - bi.m_range)), m);            
+            assumptions.push_back(lo);
+            assumptions.push_back(hi);
+            IF_VERBOSE(10, verbose_stream() << lo << "\n" << hi << "\n");
+        }
+    }
+
+    bool should_research(expr_ref_vector& unsat_core) {
+        if (!use_bounded_expansion())
+            return false;
+        bool found = false;
+        expr* t = nullptr;        
+        for (auto & e : unsat_core) {
+            if (e == m_bound_predicate) {
+                found = true;
+                for (auto & kv : m_term2bound_info) 
+                    if (kv.m_value.m_range == init_range())
+                        kv.m_value.m_range *= 2;
+            }
+            else if (m_predicate2term.find(e, t)) {
+                found = true;
+                bound_info bi;
+                VERIFY(m_term2bound_info.find(t, bi));
+                if (bi.m_range >= max_range()) {
+                    m_term2bound_info.erase(t);
+                }
+                else {
+                    bi.m_range *= 2;
+                    m_term2bound_info.insert(t, bi);
+                }
+            }
+        }
+        return found;
+    }
+
+    void add_variable_bound(expr* t, rational const& offset) {
+        if (!use_bounded_expansion())
+            return;
+        if (m_bounded_range_lit == null_literal)
+            return;
+        // if term is not already bounded, add a range and assert max_bound => range
+        bound_info bi(offset, init_range());
+        if (m_term2bound_info.find(t, bi))
+            return;
+        expr_ref hi(a.mk_le(t, a.mk_int(offset + bi.m_range)), m);
+        expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m);
+        mk_axiom(~m_bounded_range_lit, mk_literal(hi));
+        mk_axiom(~m_bounded_range_lit, mk_literal(lo));
+        m_bound_predicates.push_back(lo);
+        m_bound_predicates.push_back(hi);
+        IF_VERBOSE(10, verbose_stream() << "add " << lo << " " << hi << "\n");
+        m_predicate2term.insert(lo, t);
+        m_predicate2term.insert(hi, t);
+        m_term2bound_info.insert(t, bi);
+    }
+
 };
     
 theory_lra::theory_lra(context& ctx):
@@ -3888,8 +3995,7 @@ theory* theory_lra::mk_fresh(context* new_ctx) {
 }
 void theory_lra::init() {
     m_imp->init();
-}
+}    
-    
 bool theory_lra::internalize_atom(app * atom, bool gate_ctx) {
     return m_imp->internalize_atom(atom, gate_ctx);
 }
@@ -3997,6 +4103,13 @@ theory_var theory_lra::add_objective(app* term) {
 expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
     return m_imp->mk_ge(fm, v, val);
 }
+void theory_lra::add_theory_assumptions(expr_ref_vector& assumptions) {
+    m_imp->add_theory_assumptions(assumptions);
+}
+bool theory_lra::should_research(expr_ref_vector& unsat_core) {
+    return m_imp->should_research(unsat_core);
+}
+
 }
 template  class lp::lp_bound_propagator<smt::theory_lra::imp>;
 template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);

src/smt/theory_lra.h

@@ -95,6 +95,10 @@ namespace smt {
         
         void collect_statistics(::statistics & st) const override;
 
+        void add_theory_assumptions(expr_ref_vector& assumptions) override;
+
+        bool should_research(expr_ref_vector& unsat_core) override;
+
         // optimization
         expr_ref mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val);
         inf_eps value(theory_var) override;