debugging infinite upper bound checking

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

src/opt/optimize_objectives.cpp

@@ -70,14 +70,16 @@ namespace opt {
         arith_util autil(m);
 
         opt_solver::scoped_push _push(*s);
-        opt_solver::toggle_objective _t(*s, true);
 
         for (unsigned i = 0; i < objectives.size(); ++i) {
             m_vars.push_back(s->add_objective(objectives[i].get()));
         }
           
         lbool is_sat = l_true;
-        // ready to test: is_sat = update_upper();
+        // ready to test: 
+        is_sat = update_upper();
+        opt_solver::toggle_objective _t(*s, true);
+
         while (is_sat == l_true && !m_cancel) {
             is_sat = update_lower();
         }      
@@ -99,7 +101,8 @@ namespace opt {
                            verbose_stream() << m_lower[i] << " ";
                        }
                        verbose_stream() << "\n";
-                       model_pp(verbose_stream(), *md););
+                       // model_pp(verbose_stream(), *md);
+                       );
             expr_ref_vector disj(m);
             expr_ref constraint(m);
             
@@ -115,24 +118,38 @@ namespace opt {
 
     lbool optimize_objectives::update_upper() {
         smt::theory_opt& opt = s->get_optimizer();
-        
+
+        IF_VERBOSE(1, verbose_stream() << typeid(opt).name() << "\n";);
         if (typeid(smt::theory_inf_arith) != typeid(opt)) {
             return l_true;
         }
         smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt); 
 
         expr_ref bound(m);
+        expr_ref_vector bounds(m);
+
+        opt_solver::scoped_push _push(*s);
+        //
+        // NB: we have to create all bound expressions before calling check_sat
+        // because the state after check_sat is not at base level.
+        //
 
         for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) {
             if (m_lower[i] < m_upper[i]) {
-                opt_solver::scoped_push _push(*s);
+                SASSERT(m_upper[i].get_infinity().is_pos());
                 smt::theory_var v = m_vars[i]; 
-                // TBD: this version just works for m_upper[i] being infinity.
                 bound = th.block_upper_bound(v, m_upper[i]);
-                expr* bounds[1] = { bound };
+                bounds.push_back(bound);
-                lbool is_sat = s->check_sat(1, bounds);
+            }
+            else {
+                bounds.push_back(0);
+            }
+        }
+        for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) {
+            if (m_lower[i] < m_upper[i]) {
+                lbool is_sat = s->check_sat(1, bounds.c_ptr() + i);
                 if (is_sat == l_true) {
-                    IF_VERBOSE(1, verbose_stream() << "Setting lower bound for " << v << " to " << m_upper[i] << "\n";);
+                    IF_VERBOSE(2, verbose_stream() << "Setting lower bound for v" << m_vars[i] << " to " << m_upper[i] << "\n";);
                     m_lower[i] = m_upper[i];
                 }
                 else if (is_sat == l_false) {

src/smt/params/theory_arith_params.h

@@ -28,7 +28,8 @@ enum arith_solver_id {
     AS_ARITH,
     AS_DENSE_DIFF_LOGIC,
     AS_UTVPI,
-    AS_HORN
+    AS_HORN,
+    AS_OPTINF
 };
 
 enum bound_prop_mode {

src/smt/smt_setup.cpp

@@ -737,6 +737,9 @@ namespace smt {
             else
                 m_context.register_plugin(alloc(smt::theory_rutvpi, m_manager));          
             break;
+        case AS_OPTINF:
+            m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));            
+            break;
         default:
             if (m_params.m_arith_int_only)
                 m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));

src/smt/theory_arith.h

@@ -1067,6 +1067,7 @@ namespace smt {
         static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
             return inf_numeral(n, r);
         }
+        static bool is_infinite(inf_numeral const& ) { return false; }
         mi_ext() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {}
     };
 
@@ -1083,6 +1084,8 @@ namespace smt {
             UNREACHABLE();
             return inf_numeral(n);
         }
+        static bool is_infinite(inf_numeral const& ) { return false; }
+
         i_ext() : m_int_epsilon(1), m_real_epsilon(1) {}
     };
 
@@ -1099,6 +1102,8 @@ namespace smt {
             UNREACHABLE();
             return inf_numeral(n);
         }
+        static bool is_infinite(inf_numeral const& ) { return false; }
+
         si_ext(): m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(1)) {}
     };
     
@@ -1119,6 +1124,8 @@ namespace smt {
         static inf_numeral mk_inf_numeral(numeral const& n, numeral const& i) {
             return inf_numeral(n, i);
         }
+        static bool is_infinite(inf_numeral const& ) { return false; }
+
         smi_ext() : m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(0), true) {}
     };
 
@@ -1138,6 +1145,10 @@ namespace smt {
         static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
             return inf_numeral(inf_rational(n, r));
         }
+        static bool is_infinite(inf_numeral const& n) { 
+            return !n.get_infinity().is_zero(); 
+        }
+
         inf_ext() : m_int_epsilon(inf_rational(rational(1))), m_real_epsilon(inf_rational(rational(0), true)) {}
     };
 

src/smt/theory_arith_aux.h

@@ -1005,14 +1005,23 @@ namespace smt {
         ast_manager& m = get_manager();
         context& ctx = get_context();
         std::ostringstream strm;
-        strm << val << " <= " << v;
+        strm << val << " <= v" << v;
-        expr* b = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort());
+        expr* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
         bool_var bv = ctx.mk_bool_var(b);
-        atom* a = alloc(atom, bv, v, val+Ext::m_real_epsilon, A_LOWER);
+        ctx.set_var_theory(bv, get_id());
+        // ctx.set_enode_flag(bv, true);
+        inf_numeral val1 = val;
+        if (!Ext::is_infinite(val)) {
+            val1 += Ext::m_real_epsilon;
+        }
+        atom* a = alloc(atom, bv, v, val1, A_LOWER);
         m_unassigned_atoms[v]++;
         m_var_occs[v].push_back(a);
         m_atoms.push_back(a);
         insert_bv2a(bv, a);
+        TRACE("arith", tout << mk_pp(b, m) << "\n";
+              display_atom(tout, a, false);
+              display_atoms(tout););
         return b;
     }
 

src/smt/theory_arith_core.h

@@ -927,6 +927,7 @@ namespace smt {
     
     template<typename Ext>
     void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
+        TRACE("arith", tout << "v" << v << " " << is_true << "\n";);
         atom * a = get_bv2a(v);
         if (!a) return;
         SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@@ -2421,6 +2422,8 @@ namespace smt {
                     if (val == l_undef)
                         continue;
                     // TODO: check if the following line is a bottleneck
+                    TRACE("arith", tout << "v" << a->get_bool_var() << " " << (val == l_true) << "\n";);
+
                     a->assign_eh(val == l_true, get_epsilon(a->get_var()));
                     if (val != l_undef && a->get_bound_kind() == b->get_bound_kind()) {
                         SASSERT((ctx.get_assignment(bv) == l_true) == a->is_true());
@@ -2789,6 +2792,9 @@ namespace smt {
                 if (is_int(v))
                     continue;
                 inf_numeral const & val = get_value(v);
+                if (Ext::is_infinite(val)) {
+                    continue;
+                }
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;
                 if (mapping.find(value, v2)) {