From a307bd67e0e506a93aad365308a825ea6fa53834 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jan 2014 01:35:31 -0800 Subject: [PATCH] pareto take 3 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 28 +++++++++------- src/opt/optsmt.cpp | 41 +++--------------------- src/opt/optsmt.h | 8 +---- src/tactic/core/pb_preprocess_tactic.cpp | 17 ++++++++-- 4 files changed, 37 insertions(+), 57 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 797ff2151..bc173963d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -205,12 +205,7 @@ namespace opt { for (unsigned i = 0; i < bounds.size(); ++i) { for (unsigned j = 0; j < bounds.size(); ++j) { objective const& obj = m_objectives[j]; - if (obj.m_type == O_MAXIMIZE) { - bounds[i][j].second = bounds[j][j].second; - } - else { - bounds[i][j].first = bounds[j][j].first; - } + bounds[i][j].second = bounds[j][j].second; } display_bounds(verbose_stream() << "new bound\n", bounds[i]); } @@ -253,7 +248,7 @@ namespace opt { if (j > 0) { b2[j-1].second = b[j-1].second; } - display_bounds(verbose_stream() << "new bound\n", b2); + display_bounds(verbose_stream() << "refined bound\n", b2); bounds.push_back(b2); } break; @@ -268,7 +263,12 @@ namespace opt { for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; display_objective(out, obj); - out << " |-> [" << b[i].first << ":" << b[i].second << "]\n"; + if (obj.m_type == O_MAXIMIZE) { + out << " |-> [" << b[i].first << ":" << b[i].second << "]\n"; + } + else { + out << " |-> [" << -b[i].second << ":" << -b[i].first << "]\n"; + } } } @@ -506,11 +506,15 @@ namespace opt { for (unsigned i = 0; i < m_objectives.size(); ++i) { objective & obj = m_objectives[i]; switch(obj.m_type) { - case O_MINIMIZE: - obj.m_index = m_optsmt.add(obj.m_term, false); + case O_MINIMIZE: { + app_ref tmp(m); + arith_util a(m); + tmp = a.mk_uminus(obj.m_term); + obj.m_index = m_optsmt.add(tmp); break; + } case O_MAXIMIZE: - obj.m_index = m_optsmt.add(obj.m_term, true); + obj.m_index = m_optsmt.add(obj.m_term); break; case O_MAXSMT: { maxsmt& ms = *m_maxsmts.find(obj.m_id); @@ -604,6 +608,7 @@ namespace opt { return inf_eps(r); } case O_MINIMIZE: + return -m_optsmt.get_upper(obj.m_index); case O_MAXIMIZE: return m_optsmt.get_lower(obj.m_index); default: @@ -626,6 +631,7 @@ namespace opt { return inf_eps(r); } case O_MINIMIZE: + return -m_optsmt.get_lower(obj.m_index); case O_MAXIMIZE: return m_optsmt.get_upper(obj.m_index); default: diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 654d37687..3a895446d 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -340,19 +340,16 @@ namespace opt { is_sat = basic_opt(); } - IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << std::endl; - display_assignment(verbose_stream());); - return is_sat; } inf_eps optsmt::get_lower(unsigned i) const { - return m_is_max[i]?m_lower[i]:-m_upper[i]; + return m_lower[i]; } inf_eps optsmt::get_upper(unsigned i) const { - return m_is_max[i]?m_upper[i]:-m_lower[i]; + return m_upper[i]; } void optsmt::get_model(model_ref& mdl) { @@ -362,7 +359,7 @@ namespace opt { // force lower_bound(i) <= objective_value(i) void optsmt::commit_assignment(unsigned i) { inf_eps lo = m_lower[i]; - TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << lo << "\n"; + TRACE("opt", tout << "set lower bound of " << mk_pp(m_objs[i].get(), m) << " to: " << lo << "\n"; tout << get_lower(i) << ":" << get_upper(i) << "\n";); // Only assert bounds for bounded objectives if (lo.is_finite()) { @@ -370,42 +367,12 @@ namespace opt { } } - std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const { - bool is_max = m_is_max[i]; - expr_ref obj(m_objs[i], m); - if (!is_max) { - arith_util a(m); - th_rewriter rw(m); - obj = a.mk_uminus(obj); - rw(obj, obj); - } - return out << obj; - } - - void optsmt::display_assignment(std::ostream& out) const { - unsigned sz = m_objs.size(); - for (unsigned i = 0; i < sz; ++i) { - if (get_lower(i) != get_upper(i)) { - display_objective(out, i) << " |-> [" << get_lower(i) - << ":" << get_upper(i) << "]" << std::endl; - } - else { - display_objective(out, i) << " |-> " << get_lower(i) << std::endl; - } - } - } - - unsigned optsmt::add(app* t, bool is_max) { + unsigned optsmt::add(app* t) { expr_ref t1(t, m), t2(m); th_rewriter rw(m); - if (!is_max) { - arith_util a(m); - t1 = a.mk_uminus(t); - } rw(t1, t2); SASSERT(is_app(t2)); m_objs.push_back(to_app(t2)); - m_is_max.push_back(is_max); m_lower.push_back(inf_eps(rational(-1),inf_rational(0))); m_upper.push_back(inf_eps(rational(1), inf_rational(0))); return m_objs.size()-1; diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index a59977014..ccb7de1b5 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -34,7 +34,6 @@ namespace opt { vector m_lower; vector m_upper; app_ref_vector m_objs; - svector m_is_max; svector m_vars; symbol m_engine; model_ref m_model; @@ -49,15 +48,12 @@ namespace opt { lbool pareto(unsigned obj_index); - unsigned add(app* t, bool is_max); + unsigned add(app* t); void set_cancel(bool f); void updt_params(params_ref& p); - void display_assignment(std::ostream& out) const; - void display_range_assignment(std::ostream& out) const; - unsigned get_num_objectives() const { return m_objs.size(); } void commit_assignment(unsigned index); inf_eps get_lower(unsigned index) const; @@ -68,8 +64,6 @@ namespace opt { private: - std::ostream& display_objective(std::ostream& out, unsigned i) const; - lbool basic_opt(); lbool basic_lex(unsigned idx); diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 7297d767b..0103c16cc 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -152,8 +152,12 @@ public: SASSERT(g->is_well_sorted()); pc = 0; core = 0; - // TBD: bail out if cores are enabled. - // TBD: bail out if proofs are enabled/add proofs. + if (g->unsat_core_enabled()) { + throw tactic_exception("pb-preprocess does not support cores"); + } + if (g->proofs_enabled()) { + throw tactic_exception("pb-preprocess does not support proofs"); + } pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m); mc = pp; @@ -166,6 +170,7 @@ public: bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) { reset(); normalize(g); + decompose(g); if (g->inconsistent()) { return false; } @@ -300,6 +305,14 @@ private: } } + void decompose(goal_ref const& g) { + for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) { + expr* e = g->form(i); + if (pb.is_ge(e) && to_app(e)->get_num_args() > 20) { + // TBD: decompose inequality int smaller ones. + } + } + } void process_vars(unsigned i, goal_ref const& g) { expr* r, *e;