From 9734bab2056693a551c5f42a438a4df38f86268e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Nov 2013 21:10:15 -0800 Subject: [PATCH] pb theory Signed-off-by: Nikolaj Bjorner --- src/opt/opt_params.pyg | 1 + src/smt/theory_pb.cpp | 46 ++++++++++++++++++++++-------------------- src/smt/theory_pb.h | 3 ++- 3 files changed, 27 insertions(+), 23 deletions(-) diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 63c4d534a..4da07f305 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -6,6 +6,7 @@ def_module_params('opt', ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"), ('pareto', BOOL, False, 'return a Pareto front (as opposed to a bounding box)'), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), + ('debug_conflict', BOOL, False, 'debug conflict resolution'), )) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index c42010a4f..72483293e 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -26,6 +26,8 @@ Notes: namespace smt { + bool theory_pb::s_debug_conflict = false; // true; // + void theory_pb::ineq::negate() { m_lit.neg(); numeral sum = 0; @@ -396,8 +398,6 @@ namespace smt { ineqs->push_back(&c); } - - void theory_pb::collect_statistics(::statistics& st) const { st.update("pb axioms", m_stats.m_num_axioms); st.update("pb propagations", m_stats.m_num_propagations); @@ -920,7 +920,9 @@ namespace smt { tout << "\n"; display(tout, c);); - // DEBUG_CODE(resolve_conflict(conseq, c);); + if (s_debug_conflict) { + resolve_conflict(conseq, c); + } justification* js = 0; ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), @@ -934,25 +936,27 @@ namespace smt { context& ctx = get_context(); bool_var v = l.var(); unsigned lvl = ctx.get_assign_level(v); - IF_VERBOSE(0, verbose_stream() << l << "*" << coeff << " marked: " << ctx.is_marked(v) << " lvl: " << lvl << "\n";); if (!ctx.is_marked(v) && lvl > ctx.get_base_level()) { + IF_VERBOSE(0, verbose_stream() << l << "*" << coeff << " marked. lvl: " << lvl << "\n";); ctx.set_mark(v); + m_unmark.push_back(v); if (lvl == m_conflict_lvl) { ++m_num_marks; } - else { - m_lemma.m_args.push_back(std::make_pair(l, coeff)); - } + m_lemma.m_args.push_back(std::make_pair(l, coeff)); } } void theory_pb::process_ineq(ineq& c) { // TBD: create CUT. - context& ctx = get_context(); + // only process literals that were + // assigned below current index 'idx'. + context& ctx = get_context(); for (unsigned i = 0; i < c.size(); ++i) { - process_antecedent(c.lit(i), c.coeff(i)); + process_antecedent(c.lit(i), c.coeff(i)); } process_antecedent(~c.lit(), 1); + m_lemma.m_k += c.k(); } // @@ -984,7 +988,7 @@ namespace smt { // point into stack of assigned literals literal_vector const& lits = ctx.assigned_literals(); SASSERT(!lits.empty()); - unsigned idx = lits.size()-1; + unsigned idx = lits.size()-1; do { // @@ -997,6 +1001,7 @@ namespace smt { for (unsigned i = 0; i < num_lits; ++i) { process_antecedent(cls->get_literal(i), 1); } + m_lemma.m_k += 1; justification* cjs = cls->get_justification(); if (cjs) { // TBD @@ -1005,7 +1010,8 @@ namespace smt { break; } case b_justification::BIN_CLAUSE: - SASSERT(conseq.var() != js.get_literal().var()); + m_lemma.m_k += 1; + process_antecedent(~js.get_literal(), 0); process_antecedent(~js.get_literal(), 1); break; case b_justification::AXIOM: @@ -1025,8 +1031,8 @@ namespace smt { // // find the next marked variable in the assignment stack // - SASSERT(idx > 0); - SASSERT(m_num_marks > 0); + SASSERT(idx > 0); + SASSERT(m_num_marks > 0); do { conseq = lits[idx]; v = conseq.var(); @@ -1036,19 +1042,15 @@ namespace smt { js = ctx.get_justification(v); --m_num_marks; - ctx.unset_mark(v); - IF_VERBOSE(0, verbose_stream() << "unmark: " << v << "\n";); } while (m_num_marks > 0); // unset the marks on lemmas - for (unsigned i = 0; i < m_lemma.size(); ++i) { - bool_var v = m_lemma.lit(i).var(); - if (ctx.is_marked(v)) { - IF_VERBOSE(0, verbose_stream() << "unmark: " << v << "\n";); - ctx.unset_mark(v); - } - } + while (!m_unmark.empty()) { + ctx.unset_mark(m_unmark.back()); + m_unmark.pop_back(); + } + TRACE("card", display(tout, m_lemma);); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 28eb0ced6..49bd315c0 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -140,6 +140,7 @@ namespace smt { unsigned m_num_marks; unsigned m_conflict_lvl; ineq m_lemma; + svector m_unmark; void resolve_conflict(literal conseq, ineq& c); void process_antecedent(literal l, numeral coeff); void process_ineq(ineq& c); @@ -165,6 +166,6 @@ namespace smt { virtual void restart_eh(); virtual void collect_statistics(::statistics & st) const; - + static bool s_debug_conflict; }; };