From 5225ea18b7d911d5c0a57caa5dca53c645e1a770 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Dec 2013 09:04:48 +0200 Subject: [PATCH] fix lower/upper bound updates Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 23 +++++++++++++---------- src/opt/opt_context.cpp | 6 ++---- src/opt/optsmt.cpp | 3 ++- src/opt/optsmt.h | 2 +- src/opt/weighted_maxsat.cpp | 6 +++++- 5 files changed, 23 insertions(+), 17 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 13dc6e46d..7877ec7b0 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -43,28 +43,31 @@ namespace opt { struct fu_malik::imp { ast_manager& m; + solver & m_original_solver; + ref m_s; expr_ref_vector m_soft; expr_ref_vector m_orig_soft; expr_ref_vector m_aux; expr_ref_vector m_assignment; - unsigned m_upper_size; + unsigned m_upper; + unsigned m_lower; model_ref m_model; - ref m_s; - solver & m_original_solver; bool m_use_new_bv_solver; imp(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), + m_original_solver(s), m_s(&s), m_soft(soft), m_orig_soft(soft), m_aux(m), m_assignment(m), - m_original_solver(s), + m_upper(0), + m_lower(0), m_use_new_bv_solver(false) { - m_upper_size = m_soft.size() + 1; + m_upper = m_soft.size() + 1; } solver& s() { return *m_s; } @@ -156,7 +159,7 @@ namespace opt { } lbool step() { - IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper << ")\n";); expr_ref_vector assumptions(m), block_vars(m); for (unsigned i = 0; i < m_soft.size(); ++i) { assumptions.push_back(m.mk_not(m_aux[i].get())); @@ -295,14 +298,14 @@ namespace opt { lbool is_sat = l_true; do { is_sat = step(); - --m_upper_size; + --m_upper; } while (is_sat == l_false); if (is_sat == l_true) { // Get a list of satisfying m_soft s().get_model(m_model); - + m_lower = m_upper; m_assignment.reset(); for (unsigned i = 0; i < m_orig_soft.size(); ++i) { expr_ref val(m); @@ -335,10 +338,10 @@ namespace opt { return (*m_imp)(); } rational fu_malik::get_lower() const { - return rational(0); + return rational(m_imp->m_lower); } rational fu_malik::get_upper() const { - return rational(m_imp->m_upper_size); + return rational(m_imp->m_upper); } rational fu_malik::get_value() const { return rational(m_imp->m_assignment.size()); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8a70683fb..453af018e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -381,12 +381,10 @@ namespace opt { objective & obj = m_objectives[i]; switch(obj.m_type) { case O_MINIMIZE: - obj.m_index = m_optsmt.get_num_objectives(); - m_optsmt.add(obj.m_term, false); + obj.m_index = m_optsmt.add(obj.m_term, false); break; case O_MAXIMIZE: - obj.m_index = m_optsmt.get_num_objectives(); - m_optsmt.add(obj.m_term, true); + obj.m_index = m_optsmt.add(obj.m_term, true); break; case O_MAXSMT: { maxsmt& ms = *m_maxsmts.find(obj.m_id); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 3f8f1c939..66d46f17c 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -349,7 +349,7 @@ namespace opt { } } - void optsmt::add(app* t, bool is_max) { + unsigned optsmt::add(app* t, bool is_max) { expr_ref t1(t, m), t2(m); th_rewriter rw(m); if (!is_max) { @@ -362,6 +362,7 @@ namespace opt { 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; } void optsmt::updt_params(params_ref& p) { diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index c61599bb2..0de1e0319 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -47,7 +47,7 @@ namespace opt { lbool lex(unsigned obj_index); - void add(app* t, bool is_max); + unsigned add(app* t, bool is_max); void set_cancel(bool f); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index b03b8005a..97de77219 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -291,6 +291,7 @@ namespace opt { expr_ref_vector m_assignment; vector m_weights; rational m_upper; + rational m_lower; model_ref m_model; imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights): @@ -345,6 +346,9 @@ namespace opt { } } m_upper = wth.get_min_cost(); + if (result == l_true) { + m_lower = m_upper; + } wth.get_model(m_model); TRACE("opt", tout << "min cost: " << m_upper << "\n";); wth.reset(); @@ -352,7 +356,7 @@ namespace opt { } rational get_lower() const { - return rational(0); + return m_lower; } rational get_upper() const {