From eb4def108ff864a4311d8bcd0e72f7d68090ce02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2013 17:45:14 -0800 Subject: [PATCH] reinit logic Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 46 ++++++++++++++++++++++--------------- src/smt/smt_context.cpp | 2 +- src/smt/theory_pb.cpp | 17 ++++++++++---- src/smt/theory_pb.h | 2 ++ 4 files changed, 43 insertions(+), 24 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 863cab7ef..439d853c7 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -367,6 +367,15 @@ namespace opt { ~imp() {} + void re_init(expr_ref_vector const& soft, vector const& weights) { + m_soft.reset(); + m_soft.append(soft); + m_weights.reset(); + m_weights.append(weights); + m_assignment.reset(); + m_assignment.resize(m_soft.size(), false); + } + smt::theory_weighted_maxsat* get_theory() const { smt::context& ctx = s.get_context(); smt::theory_id th_id = m.get_family_id("weighted_maxsat"); @@ -601,17 +610,18 @@ namespace opt { lbool pb_solve() { pb_util u(m); expr_ref fml(m), val(m); + app_ref b(m); expr_ref_vector nsoft(m); m_lower = m_upper = rational::zero(); - rational minw(0); + solver::scoped_push __s(s); for (unsigned i = 0; i < m_soft.size(); ++i) { m_upper += m_weights[i]; - if (m_weights[i] < minw || minw.is_zero()) { - minw = m_weights[i]; - } - nsoft.push_back(m.mk_not(m_soft[i].get())); + b = m.mk_fresh_const("b", m.mk_bool_sort()); + s.mc().insert(b->get_decl()); + fml = m.mk_or(m_soft[i].get(), b); + s.assert_expr(fml); + nsoft.push_back(b); } - solver::scoped_push __s(s); lbool is_sat = l_true; bool was_sat = false; while (l_true == is_sat) { @@ -623,14 +633,14 @@ namespace opt { s.get_model(m_model); m_upper = rational::zero(); for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(m_model->eval(m_soft[i].get(), val)); - m_assignment[i] = !m.is_false(val); + VERIFY(m_model->eval(nsoft[i].get(), val)); + m_assignment[i] = !m.is_true(val); if (!m_assignment[i]) { m_upper += m_weights[i]; } } - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";); - fml = u.mk_le(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper - minw); + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << " )\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); s.assert_expr(fml); was_sat = true; } @@ -854,9 +864,8 @@ namespace opt { } for (unsigned i = 0; i < bs.size(); ++i) { nbs.push_back(m.mk_not(bs[i])); - } - m_imp = alloc(imp, m, m_solver, nbs, ws); // race condition. - m_imp->updt_params(m_params); + } + m_imp->re_init(nbs, ws); lbool is_sat = m_imp->pb_simplify_solve(); k = m_imp->m_lower; m_solver.pop_core(1); @@ -903,9 +912,9 @@ namespace opt { m_solver.assert_expr(r->form(i)); } is_sat = m_solver.check_sat_core(0, 0); - if (l_true == is_sat) { + if (l_true == is_sat && !m_cancel) { m_solver.get_model(m_model); - if (mc) (*mc)(m_model, 0); + if (mc && m_model) (*mc)(m_model, 0); IF_VERBOSE(2, g->display(verbose_stream() << "goal:\n"); r->display(verbose_stream() << "reduced:\n"); @@ -919,6 +928,7 @@ namespace opt { wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights) { m_imp = alloc(imp, m, s, soft_constraints, weights); + m_imp->m_imp = alloc(imp, m, m_imp->m_solver, soft_constraints, weights); } wmaxsmt::~wmaxsmt() { @@ -940,10 +950,8 @@ namespace opt { void wmaxsmt::set_cancel(bool f) { m_imp->m_cancel = f; m_imp->m_solver.set_cancel(f); - // TBD race - if (m_imp->m_imp) { - m_imp->m_imp->m_cancel = f; - } + m_imp->m_imp->m_cancel = f; + m_imp->m_imp->m_solver.set_cancel(f); } void wmaxsmt::collect_statistics(statistics& st) const { m_imp->m_solver.collect_statistics(st); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 2cce3931e..8c8d7040d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3238,7 +3238,7 @@ namespace smt { for (; it != end; ++it) (*it)->restart_eh(); TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); - m_qmanager->restart_eh(); + m_qmanager->restart_eh(); } if (m_fparams.m_simplify_clauses) simplify_clauses(); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index c04390ea8..d40869dc0 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -209,7 +209,7 @@ namespace smt { break; } -#if 0 +#if 1 // TBD: special cases: k == 1, or args.size() == 1 if (c->k().is_one()) { @@ -236,7 +236,7 @@ namespace smt { // pre-compile threshold for cardinality bool is_cardinality = true; for (unsigned i = 0; is_cardinality && i < args.size(); ++i) { - is_cardinality = (args[i].second.is_one()); + is_cardinality = (args[i].second < rational(8)); } if (is_cardinality) { unsigned log = 1, n = 1; @@ -373,6 +373,8 @@ namespace smt { st.update("pb propagations", m_stats.m_num_propagations); st.update("pb predicates", m_stats.m_num_predicates); st.update("pb compilations", m_stats.m_num_compiles); + st.update("pb compiled clauses", m_stats.m_num_compiled_clauses); + st.update("pb compiled vars", m_stats.m_num_compiled_vars); } void theory_pb::reset_eh() { @@ -694,6 +696,7 @@ namespace smt { } else { l = literal(ctx.mk_bool_var(t)); + ++th.m_stats.m_num_compiled_vars; } add_clause(~l, ~a, b); add_clause(~l, a, c); @@ -719,6 +722,7 @@ namespace smt { TRACE("pb", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX, 0); + ++th.m_stats.m_num_compiled_clauses; } void add_clause(literal l1, literal l2) { @@ -749,7 +753,7 @@ namespace smt { context& ctx = get_context(); // only cardinality constraints are compiled. SASSERT(c.m_compilation_threshold < UINT_MAX); - DEBUG_CODE(for (unsigned i = 0; i < c.size(); ++i) SASSERT(c.coeff(i).is_one()); ); + DEBUG_CODE(for (unsigned i = 0; i < c.size(); ++i) SASSERT(c.coeff(i).is_int()); ); unsigned k = c.k().get_unsigned(); unsigned num_args = c.size(); @@ -758,9 +762,14 @@ namespace smt { expr_ref_vector in(m), out(m); expr_ref tmp(m); for (unsigned i = 0; i < num_args; ++i) { + rational n = c.coeff(i); ctx.literal2expr(c.lit(i), tmp); - in.push_back(tmp); + while (n.is_pos()) { + in.push_back(tmp); + n -= rational::one(); + } } + IF_VERBOSE(1, verbose_stream() << "(compile " << k << ")\n";); sn(in, out); literal at_least_k = se.internalize(c, out[k-1].get()); // first k outputs are 1. TRACE("pb", tout << "at_least: " << mk_pp(out[k-1].get(), m) << "\n";); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 66a8eccba..8f79f0494 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -38,6 +38,8 @@ namespace smt { unsigned m_num_propagations; unsigned m_num_predicates; unsigned m_num_compiles; + unsigned m_num_compiled_vars; + unsigned m_num_compiled_clauses; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } };