From c84ab2fc017a169299cd5d2e855fcc2cf84c6e31 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Apr 2014 22:12:22 -0700 Subject: [PATCH] tidy Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index af97c57a0..36242543d 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -126,7 +126,7 @@ namespace opt { obj_map ans2core; // answer literal to core index lbool is_sat = l_undef; expr_ref_vector rs(m), asms(m); - vector sigmas; // sigma_j := w_j if soft clause has not been satisfied + vector sigmas(m_weights); // sigma_j := w_j if soft clause has not been satisfied bool first = true; init(); for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -136,9 +136,9 @@ namespace opt { s().assert_expr(fml); // does not get asserted in model-based mode. rs.push_back(r); asms.push_back(m.mk_not(r)); - sigmas.push_back(m_weights[i]); + SASSERT(m_weights[i].is_int()); // TBD: re-normalize weights if non-integral. } - m_upper += rational(1); + m_upper += rational(1); // TBD: assuming integral weights solver::scoped_push _s(s()); while (m_lower < m_upper) { solver::scoped_push __s(s()); @@ -783,8 +783,7 @@ namespace opt { final_check that satisfies min_cost. Takes: log (n / log(n)) iterations - */ - + */ class iwmax : public maxsmt_solver_wbase { public: