From af55088b7852f1027df86380ccf7b6f5b8b3c438 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Mar 2014 10:34:32 -0700 Subject: [PATCH] debugging opt Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb_rewriter_def.h | 2 +- src/opt/opt_context.cpp | 7 ++- src/opt/opt_params.pyg | 3 +- src/opt/weighted_maxsat.cpp | 76 +++++++++++++++++++----- src/smt/params/theory_pb_params.h | 2 +- src/smt/theory_pb.cpp | 14 +++-- src/tactic/arith/lia2card_tactic.cpp | 20 ++++--- src/tactic/arith/purify_arith_tactic.cpp | 2 +- 8 files changed, 92 insertions(+), 34 deletions(-) diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h index 3c60babce..af19e46e6 100644 --- a/src/ast/rewriter/pb_rewriter_def.h +++ b/src/ast/rewriter/pb_rewriter_def.h @@ -141,7 +141,7 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: for (unsigned i = 0; i < args.size(); ++i) { args[i].second = PBU::numeral::one(); } - k = PBU::numeral::one(); + k = PBU::numeral(args.size()); return l_undef; } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index bf80044d6..22cbf21cc 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -310,10 +310,13 @@ namespace opt { mk_solve_eqs_tactic(m), mk_elim_uncnstr_tactic(m), mk_simplify_tactic(m)); - tactic_ref tac2 = mk_elim01_tactic(m); - tactic_ref tac3 = mk_lia2card_tactic(m); opt_params optp(m_params); if (optp.elim_01()) { + tactic_ref tac2 = mk_elim01_tactic(m); + tactic_ref tac3 = mk_lia2card_tactic(m); + params_ref lia_p; + lia_p.set_bool("compile_equality", optp.pb_compile_equality()); + tac3->updt_params(lia_p); m_simplify = and_then(tac0.get(), tac2.get(), tac3.get()); } else { diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 188e3a416..7d6e55a82 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -10,7 +10,8 @@ def_module_params('opt', ('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'), ('debug_conflict', BOOL, False, 'debug conflict resolution'), ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'iwmax' (iterative), 'bwmax' (bisection)"), - ('elim_01', BOOL, True, 'eliminate 01 variables') + ('elim_01', BOOL, True, 'eliminate 01 variables'), + ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)') )) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index dcf9313b5..dde454941 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -266,7 +266,6 @@ namespace smt { m_min_cost_atoms.reset(); m_propagate = false; m_assigned.reset(); - m_stats.reset(); } virtual theory * mk_fresh(context * new_ctx) { return 0; } @@ -300,6 +299,7 @@ namespace smt { } expr_ref mk_block() { + ++m_stats.m_num_blocks; ast_manager& m = get_manager(); expr_ref_vector disj(m); compare_cost compare_cost(*this); @@ -445,6 +445,8 @@ namespace opt { m_weights.append(weights); m_assignment.reset(); m_assignment.resize(m_soft.size(), false); + m_lower.reset(); + m_upper.reset(); } smt::theory_weighted_maxsat* get_theory() const { @@ -686,18 +688,28 @@ namespace opt { return is_sat; } + expr* mk_not(expr* e) { + if (m.is_not(e, e)) { + return e; + } + else { + return m.mk_not(e); + } + } + lbool pb_simplify_solve() { + TRACE("opt", s.display(tout); tout << "\n"; + for (unsigned i = 0; i < m_soft.size(); ++i) { + tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; + } + ); pb_util u(m); expr_ref fml(m), val(m); expr_ref_vector nsoft(m); m_lower = m_upper = rational::zero(); - rational minw(0); 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())); + nsoft.push_back(mk_not(m_soft[i].get())); } solver::scoped_push _s1(s); lbool is_sat = l_true; @@ -711,17 +723,18 @@ namespace opt { is_sat = l_undef; } if (is_sat == l_true) { - rational old_upper = m_upper; 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); + TRACE("opt", tout << "eval " << mk_pp(m_soft[i].get(), m) << " " << val << "\n";); + 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); + TRACE("opt", tout << "new upper: " << m_upper << "\n";); + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); was_sat = true; } } @@ -729,6 +742,7 @@ namespace opt { is_sat = l_true; m_lower = m_upper; } + TRACE("opt", tout << "lower: " << m_lower << "\n";); return is_sat; } @@ -777,6 +791,20 @@ namespace opt { asms.append(ans); asms.append(am); lbool is_sat = s.check_sat(asms.size(), asms.c_ptr()); + TRACE("opt", + tout << "\nassumptions: "; + for (unsigned i = 0; i < asms.size(); ++i) { + tout << mk_pp(asms[i].get(), m) << " "; + } + tout << "\n" << is_sat << "\n"; + tout << "upper: " << m_upper << "\n"; + tout << "lower: " << m_lower << "\n"; + if (is_sat == l_true) { + model_ref mdl; + s.get_model(mdl); + model_smt2_pp(tout, m, *(mdl.get()), 0); + }); + if (m_cancel && is_sat != l_false) { is_sat = l_undef; } @@ -784,17 +812,24 @@ namespace opt { m_upper = m_lower; updt_model(s); for (unsigned i = 0; i < block.size(); ++i) { - VERIFY(m_model->eval(block[i].get(), val)); - m_assignment[i] = m.is_false(val); + VERIFY(m_model->eval(m_soft[i].get(), val)); + TRACE("opt", tout << mk_pp(block[i].get(), m) << " " << val << "\n";); + m_assignment[i] = m.is_true(val); } } - if (is_sat != l_false) { + if (is_sat != l_false) { return is_sat; } s.get_unsat_core(core); if (core.empty()) { return l_false; } + TRACE("opt", + tout << "core: "; + for (unsigned i = 0; i < core.size(); ++i) { + tout << mk_pp(core[i],m) << " "; + } + tout << "\n";); uint_set A; for (unsigned i = 0; i < core.size(); ++i) { unsigned j; @@ -834,6 +869,7 @@ namespace opt { if (is_sat != l_true) { return is_sat; } + TRACE("opt", tout << "new bound: " << k << " lower: " << m_lower << "\n";); m_lower += k; expr_ref B_le_k(m), B_ge_k(m); B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k); @@ -1031,7 +1067,9 @@ namespace opt { rational& k) { pb_util u(m); lbool is_sat = bound(al, ws, bs, k); - if (is_sat != l_true) return is_sat; + if (is_sat != l_true || !k.is_zero()) { + return is_sat; + } expr_ref_vector al2(m); al2.append(al); // w_j*b_j > k @@ -1054,8 +1092,14 @@ namespace opt { m_solver.assert_expr(al[i]); } for (unsigned i = 0; i < bs.size(); ++i) { - nbs.push_back(m.mk_not(bs[i])); + nbs.push_back(mk_not(bs[i])); } + TRACE("opt", + m_solver.display(tout); + tout << "\n"; + for (unsigned i = 0; i < bs.size(); ++i) { + tout << mk_pp(bs[i], m) << " " << ws[i] << "\n"; + }); m_imp->re_init(nbs, ws); lbool is_sat = m_imp->pb_simplify_solve(); k = m_imp->m_lower; @@ -1105,7 +1149,7 @@ namespace opt { } else { SASSERT(result.size() == 1); - goal* r = result[0]; + goal_ref r = result[0]; solver::scoped_push _s(m_solver); // TBD ptr_vector asms; for (unsigned i = 0; i < r->size(); ++i) { diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h index 03deb8930..f6debea8a 100644 --- a/src/smt/params/theory_pb_params.h +++ b/src/smt/params/theory_pb_params.h @@ -31,7 +31,7 @@ struct theory_pb_params { m_pb_conflict_frequency(0), m_pb_learn_complements(true), m_pb_enable_compilation(true), - m_pb_enable_simplex(false) + m_pb_enable_simplex(false) {} void updt_params(params_ref const & p); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 176fb66a4..b5fadac7c 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -388,16 +388,13 @@ namespace smt { } } - // m_simplex.display(std::cout); literal_vector lits; for (unsigned i = 0; i < explains.size(); ++i) { literal lit(explains[i]); if (lit != null_literal) { - //std::cout << lit << " "; lits.push_back(~lit); } } - //std::cout << "\n"; m_stats.m_num_conflicts++; justification* js = 0; @@ -799,8 +796,11 @@ namespace smt { unsigned slack = info.m_slack; if (is_true) { update_bound(slack, literal(v), true, coeff); + if (c->is_eq()) { + update_bound(slack, literal(v), false, coeff); + } } - else { + else if (c->is_ge()) { m_mpq_inf_mgr.sub(coeff, std::make_pair(mpq(1),mpq(0)), coeff); update_bound(slack, ~literal(v), false, coeff); } @@ -1678,10 +1678,14 @@ namespace smt { if (!conseq.sign() && j->get_from_theory() == get_id()) { pbj = dynamic_cast(j); } - if (pbj && pbj->get_ineq().is_ge()) { + if (pbj && pbj->get_ineq().is_eq()) { // only resolve >= that are positive consequences. pbj = 0; } + if (pbj && pbj->get_ineq().lit() == conseq) { + // can't resolve against literal representing inequality. + pbj = 0; + } if (pbj) { // weaken the lemma and resolve. TRACE("pb", display(tout << "resolve with inequality", pbj->get_ineq(), true);); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index a819791ec..7ed867155 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -33,12 +33,13 @@ public: pb_util m_pb; mutable ptr_vector m_todo; expr_set m_01s; - + bool m_compile_equality; lia2card_tactic(ast_manager & _m, params_ref const & p): m(_m), a(m), - m_pb(m) { + m_pb(m), + m_compile_equality(false) { } virtual ~lia2card_tactic() { @@ -49,6 +50,7 @@ public: void updt_params(params_ref const & p) { m_params = p; + m_compile_equality = p.get_bool("compile_equality", false); } virtual void operator()(goal_ref const & g, @@ -64,6 +66,7 @@ public: bound_manager bounds(m); bounds(*g); + bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); for (; bit != bend; ++bit) { @@ -175,11 +178,12 @@ public: } expr* mk_eq(unsigned sz, rational const* weights, expr* const* args, rational const& w) { -#if 1 - return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w)); -#else - return m_pb.mk_eq(sz, weights, args, w); -#endif + if (m_compile_equality) { + return m_pb.mk_eq(sz, weights, args, w); + } + else { + return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w)); + } } expr* mk_ge(unsigned sz, rational const* weights, expr* const* args, rational const& w) { @@ -270,6 +274,8 @@ public: } virtual void collect_param_descrs(param_descrs & r) { + r.insert("compile_equality", CPK_BOOL, + "(default:false) compile equalities into pseudo-Boolean equality"); } virtual void cleanup() { diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index f2ddd86ce..e18c6e90b 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -707,7 +707,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { r.insert("complete", CPK_BOOL, - "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a functio. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root"); + "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root"); r.insert("elim_root_objects", CPK_BOOL, "(default: true) eliminate root objects."); r.insert("elim_inverses", CPK_BOOL,