From 99b4ce037d1c300e87f87e361a1332accd1e041b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Mar 2014 16:29:26 -0800 Subject: [PATCH] integrating diff opt Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 13 +++++++++---- src/opt/opt_context.h | 2 ++ src/opt/opt_solver.cpp | 25 +++++++------------------ src/opt/opt_solver.h | 5 ++--- src/opt/optsmt.cpp | 24 +++++++++--------------- src/smt/theory_arith.h | 5 +++-- src/smt/theory_arith_aux.h | 18 ++++++++++++------ src/smt/theory_diff_logic.h | 4 ++-- src/smt/theory_diff_logic_def.h | 27 ++++++++++++++++++++------- src/smt/theory_opt.h | 3 +-- 10 files changed, 67 insertions(+), 59 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 3399854a5..bf80044d6 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -312,18 +312,17 @@ namespace opt { mk_simplify_tactic(m)); tactic_ref tac2 = mk_elim01_tactic(m); tactic_ref tac3 = mk_lia2card_tactic(m); - tactic_ref tac; opt_params optp(m_params); if (optp.elim_01()) { - tac = and_then(tac0.get(), tac2.get(), tac3.get()); + m_simplify = and_then(tac0.get(), tac2.get(), tac3.get()); } else { - tac = tac0.get(); + m_simplify = tac0.get(); } proof_converter_ref pc; expr_dependency_ref core(m); goal_ref_buffer result; - (*tac)(g, result, m_model_converter, pc, core); // TBD: have this an attribute so we can cancel. + (*m_simplify)(g, result, m_model_converter, pc, core); SASSERT(result.size() == 1); goal* r = result[0]; fmls.reset(); @@ -708,6 +707,9 @@ namespace opt { if (m_solver) { m_solver->set_cancel(f); } + if (m_simplify) { + m_simplify->set_cancel(f); + } m_optsmt.set_cancel(f); map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); for (; it != end; ++it) { @@ -719,6 +721,9 @@ namespace opt { if (m_solver) { m_solver->collect_statistics(stats); } + if (m_simplify) { + m_simplify->collect_statistics(stats); + } map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); for (; it != end; ++it) { it->m_value->collect_statistics(stats); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 4afa676f5..be323073e 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -30,6 +30,7 @@ Notes: #include "optsmt.h" #include "maxsmt.h" #include "model_converter.h" +#include "tactic.h" namespace opt { @@ -89,6 +90,7 @@ namespace opt { obj_map m_objective_fns; obj_map m_objective_orig; func_decl_ref_vector m_objective_refs; + tactic_ref m_simplify; public: context(ast_manager& m); ~context(); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 699a7898c..bf5fe0765 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -133,15 +133,17 @@ namespace opt { return r; } - void opt_solver::maximize_objectives() { + void opt_solver::maximize_objectives(expr_ref_vector& blockers) { + expr_ref blocker(m); for (unsigned i = 0; i < m_objective_vars.size(); ++i) { - maximize_objective(i); + maximize_objective(i, blocker); + blockers.push_back(blocker); } } - void opt_solver::maximize_objective(unsigned i) { + void opt_solver::maximize_objective(unsigned i, expr_ref& blocker) { smt::theory_var v = m_objective_vars[i]; - m_objective_values[i] = get_optimizer().maximize(v); + m_objective_values[i] = get_optimizer().maximize(v, blocker); m_context.get_context().update_model(); TRACE("opt", { model_ref mdl; get_model(mdl); model_smt2_pp(tout << "update model: ", m, *mdl, 0); }); } @@ -231,20 +233,7 @@ namespace opt { // difference logic? return expr_ref(m.mk_true(), m); - } - - expr_ref opt_solver::mk_gt(unsigned var, inf_eps const& val) { - if (val.get_infinity().is_pos()) { - return expr_ref(m.mk_false(), m); - } - else if (val.get_infinity().is_neg()) { - return expr_ref(m.mk_true(), m); - } - else { - inf_rational n = val.get_numeral(); - return expr_ref(get_optimizer().mk_gt(m_objective_vars[var], n), m); - } - } + } void opt_solver::reset_objectives() { m_objective_vars.reset(); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 0f62642d4..74d75a806 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -75,12 +75,11 @@ namespace opt { smt::theory_var add_objective(app* term); void reset_objectives(); - void maximize_objective(unsigned i); - void maximize_objectives(); + void maximize_objective(unsigned i, expr_ref& blocker); + void maximize_objectives(expr_ref_vector& blockers); vector const& get_objective_values(); inf_eps const & get_objective_value(unsigned obj_index); - expr_ref mk_gt(unsigned obj_index, inf_eps const& val); expr_ref mk_ge(unsigned obj_index, inf_eps const& val); filter_model_converter& mc() { return m_fm; } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index c1fc60de2..26f8116a0 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -124,7 +124,8 @@ namespace opt { } void optsmt::update_lower() { - m_s->maximize_objectives(); + expr_ref_vector disj(m); + m_s->maximize_objectives(disj); m_s->get_model(m_model); set_max(m_lower, m_s->get_objective_values()); IF_VERBOSE(1, @@ -134,13 +135,7 @@ namespace opt { verbose_stream() << "\n"; model_pp(verbose_stream(), *m_model); ); - expr_ref_vector disj(m); - expr_ref constraint(m); - - for (unsigned i = 0; i < m_lower.size(); ++i) { - inf_eps const& v = m_lower[i]; - disj.push_back(m_s->mk_gt(i, v)); - } + expr_ref constraint(m); constraint = m.mk_or(disj.size(), disj.c_ptr()); m_s->assert_expr(constraint); } @@ -237,25 +232,23 @@ namespace opt { lbool optsmt::basic_lex(unsigned obj_index) { lbool is_sat = l_true; - expr_ref block(m); - + expr_ref block(m), tmp(m); while (is_sat == l_true && !m_cancel) { is_sat = m_s->check_sat(0, 0); if (is_sat != l_true) break; - m_s->maximize_objective(obj_index); + m_s->maximize_objective(obj_index, block); m_s->get_model(m_model); inf_eps obj = m_s->get_objective_value(obj_index); if (obj > m_lower[obj_index]) { m_lower[obj_index] = obj; IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";); for (unsigned i = obj_index+1; i < m_vars.size(); ++i) { - m_s->maximize_objective(i); + m_s->maximize_objective(i, tmp); m_lower[i] = m_s->get_objective_value(i); } } - block = m_s->mk_gt(obj_index, obj); m_s->assert_expr(block); // TBD: only works for simplex @@ -289,14 +282,13 @@ namespace opt { is_sat = m_s->check_sat(0, 0); if (is_sat != l_true) break; was_sat = true; - m_s->maximize_objective(obj_index); + m_s->maximize_objective(obj_index, block); m_s->get_model(m_model); inf_eps obj = m_s->get_objective_value(obj_index); if (obj > m_lower[obj_index]) { m_lower[obj_index] = obj; IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";); } - block = m_s->mk_gt(obj_index, obj); m_s->assert_expr(block); } @@ -347,10 +339,12 @@ namespace opt { inf_eps optsmt::get_lower(unsigned i) const { + if (i >= m_lower.size()) return inf_eps(); return m_lower[i]; } inf_eps optsmt::get_upper(unsigned i) const { + if (i >= m_upper.size()) return inf_eps(); return m_upper[i]; } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index ee2ce349d..2e8c62393 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -998,9 +998,8 @@ namespace smt { // Optimization // // ----------------------------------- - virtual inf_eps_rational maximize(theory_var v); + virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker); virtual theory_var add_objective(app* term); - virtual expr* mk_gt(theory_var v, inf_rational const& val); virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val); void enable_record_conflict(expr* bound); void record_conflict(unsigned num_lits, literal const * lits, @@ -1008,6 +1007,8 @@ namespace smt { unsigned num_params, parameter* params); inf_eps_rational conflict_minimize(); private: + virtual expr_ref mk_gt(theory_var v); + bool_var m_bound_watch; inf_eps_rational m_upper_bound; bool get_theory_vars(expr * n, uint_set & vars); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index eeafb1aa5..7e397dbe5 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1065,13 +1065,17 @@ namespace smt { } template - inf_eps_rational theory_arith::maximize(theory_var v) { + inf_eps_rational theory_arith::maximize(theory_var v, expr_ref& blocker) { TRACE("opt", tout << "data-size: " << m_data.size() << "\n";); max_min_t r = max_min(v, true); if (r == UNBOUNDED) { + blocker = get_manager().mk_false(); return inf_eps_rational::infinity(); } - return inf_eps_rational(get_value(v)); + else { + blocker = mk_gt(v); + return inf_eps_rational(get_value(v)); + } } @@ -1081,8 +1085,9 @@ namespace smt { for the theory of aritmetic. */ template - expr* theory_arith::mk_gt(theory_var v, inf_rational const& val) { + expr_ref theory_arith::mk_gt(theory_var v) { ast_manager& m = get_manager(); + inf_numeral const& val = get_value(v); expr* obj = get_enode(v)->get_owner(); expr_ref e(m); rational r = val.get_rational(); @@ -1094,19 +1099,20 @@ namespace smt { r = ceil(r); } e = m_util.mk_numeral(r, m.get_sort(obj)); - return m_util.mk_ge(obj, e); + e = m_util.mk_ge(obj, e); } else { // obj is over the reals. e = m_util.mk_numeral(r, m.get_sort(obj)); if (val.get_infinitesimal().is_neg()) { - return m_util.mk_ge(obj, e); + e = m_util.mk_ge(obj, e); } else { - return m_util.mk_gt(obj, e); + e = m_util.mk_gt(obj, e); } } + return e; } /** diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 91cf9796f..b9578657c 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -308,9 +308,9 @@ namespace smt { // // ----------------------------------- - virtual inf_eps_rational maximize(theory_var v); + virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker); virtual theory_var add_objective(app* term); - virtual expr* mk_gt(theory_var v, inf_rational const& val); + virtual expr_ref mk_gt(theory_var v, inf_rational const& val); virtual expr* mk_ge(theory_var v, inf_rational const& val) { return 0; } bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 875a3ff94..e7167b2cd 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -999,10 +999,11 @@ void theory_diff_logic::get_implied_bound_antecedents(edge_id bridge_edge, } template -inf_eps_rational theory_diff_logic::maximize(theory_var v) { +inf_eps_rational theory_diff_logic::maximize(theory_var v, expr_ref& blocker) { typedef simplex::simplex Simplex; Simplex S; + ast_manager& m = get_manager(); objective_term const& objective = m_objectives[v]; IF_VERBOSE(1, @@ -1067,30 +1068,37 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { // optimize lbool is_sat = S.make_feasible(); if (is_sat == l_undef) { + blocker = m.mk_false(); return inf_eps_rational::infinity(); } - TRACE("opt", S.display(tout); ); + TRACE("opt", S.display(tout); ); SASSERT(is_sat != l_false); lbool is_fin = S.minimize(w); switch (is_fin) { case l_true: { simplex::mpq_ext::eps_numeral const& val = S.get_value(w); inf_rational r(-rational(val.first), -rational(val.second)); - TRACE("opt", tout << r << " " << "\n"; ); + TRACE("opt", tout << r << " " << "\n"; + S.display_row(tout, row, true);); Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row); - S.display_row(std::cout, row, true); + expr_ref_vector& core = m_objective_assignments[v]; + expr_ref tmp(m); + core.reset(); for (; it != end; ++it) { unsigned v = it->m_var; if (num_nodes <= v && v < num_nodes + num_edges) { unsigned edge_id = v - num_nodes; literal lit = m_graph.get_explanation(edge_id); - std::cout << lit << "\n"; + get_context().literal2expr(lit, tmp); + core.push_back(tmp); } } + blocker = mk_gt(v, r); return inf_eps_rational(rational(0), r); } default: TRACE("opt", tout << "unbounded\n"; ); + blocker = m.mk_false(); return inf_eps_rational::infinity(); } } @@ -1135,7 +1143,9 @@ expr_ref theory_diff_logic::block_objective(theory_var v, inf_rational cons } else { // - f = m.mk_true(); + expr_ref_vector const& core = m_objective_assignments[v]; + f = m.mk_not(m.mk_and(core.size(), core.c_ptr())); + TRACE("arith", tout << "block: " << f << "\n";); return f; } @@ -1152,8 +1162,10 @@ expr_ref theory_diff_logic::block_objective(theory_var v, inf_rational cons } template -expr* theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) { +expr_ref theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) { expr_ref o = block_objective(v, val); + return o; +#if 0 context & ctx = get_context(); model_ref mdl; ctx.get_model(mdl); @@ -1162,6 +1174,7 @@ expr* theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) { model_implicant impl_extractor(m); expr_ref_vector implicants = impl_extractor.minimize_literals(formulas, mdl); return m.mk_and(o, m.mk_not(m.mk_and(implicants.size(), implicants.c_ptr()))); +#endif } template diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index 2d4d33e20..cf000143f 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -29,9 +29,8 @@ namespace smt { class theory_opt { public: typedef inf_eps_rational inf_eps; - virtual inf_eps maximize(theory_var v) { UNREACHABLE(); return inf_eps::infinity(); } + virtual inf_eps maximize(theory_var v, expr_ref& blocker) = 0; // { UNREACHABLE(); return inf_eps::infinity(); } virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } - virtual expr* mk_gt(theory_var v, inf_rational const& val) { UNREACHABLE(); return 0; } virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; } }; }