From 3c6f0c737ad62f8ce532673bc21a9af3e813782f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Nov 2013 17:26:27 -0700 Subject: [PATCH] debugging infinite upper bound checking Signed-off-by: Nikolaj Bjorner --- src/opt/optimize_objectives.cpp | 35 +++++++++++++++++++++------- src/smt/params/theory_arith_params.h | 3 ++- src/smt/smt_setup.cpp | 3 +++ src/smt/theory_arith.h | 11 +++++++++ src/smt/theory_arith_aux.h | 15 +++++++++--- src/smt/theory_arith_core.h | 6 +++++ 6 files changed, 60 insertions(+), 13 deletions(-) diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index f9ebe8b7b..bcc2b52be 100644 --- a/src/opt/optimize_objectives.cpp +++ b/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(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 }; - lbool is_sat = s->check_sat(1, bounds); + bounds.push_back(bound); + } + 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) { diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 30bc65b6d..b02ae3980 100644 --- a/src/smt/params/theory_arith_params.h +++ b/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 { diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index f91a58f87..52ad14155 100644 --- a/src/smt/smt_setup.cpp +++ b/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)); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 56c361a93..724cce200 100644 --- a/src/smt/theory_arith.h +++ b/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)) {} }; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 09ab33c93..e864db589 100644 --- a/src/smt/theory_arith_aux.h +++ b/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; - expr* b = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort()); + strm << val << " <= v" << v; + 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; } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 11484c779..983d0a9ea 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -927,6 +927,7 @@ namespace smt { template void theory_arith::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)) {