From 26237a37272169deac6dfb333fddc6a5e6afd4d6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Dec 2013 07:40:18 +0200 Subject: [PATCH] debug benchmarks, theory_pb Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 4 +- src/opt/weighted_maxsat.cpp | 10 ++- src/smt/theory_pb.cpp | 116 +++++++++++++++++++++------ src/smt/theory_pb.h | 2 + src/tactic/arith/lia2card_tactic.cpp | 6 ++ 5 files changed, 108 insertions(+), 30 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 599b6d7d2..3cbc3d3a1 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -27,6 +27,7 @@ Notes: #include "tactic.h" #include "lia2card_tactic.h" #include "elim01_tactic.h" +#include "simplify_tactic.h" #include "tactical.h" #include "model_smt2_pp.h" @@ -189,9 +190,10 @@ namespace opt { for (unsigned i = 0; i < fmls.size(); ++i) { g->assert_expr(fmls[i].get()); } + tactic_ref tac0 = mk_simplify_tactic(m); tactic_ref tac1 = mk_elim01_tactic(m); tactic_ref tac2 = mk_lia2card_tactic(m); - tactic_ref tac = and_then(tac1.get(), tac2.get()); + tactic_ref tac = and_then(tac0.get(), tac1.get(), tac2.get()); proof_converter_ref pc; expr_dependency_ref core(m); goal_ref_buffer result; diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 1d2aa22a6..427725fbe 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -253,7 +253,7 @@ namespace smt { disj.push_back(m.mk_not(m_min_cost_atom)); } if (is_optimal()) { - IF_VERBOSE(1, verbose_stream() << "(wmaxsat with lower bound: " << weight << "\n";); + IF_VERBOSE(1, verbose_stream() << "(wmaxsat with lower bound: " << weight << ")\n";); m_min_cost = weight; m_cost_save.reset(); m_cost_save.append(m_costs); @@ -363,9 +363,10 @@ namespace opt { rational m_upper; rational m_lower; model_ref m_model; + volatile bool m_cancel; imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights): - m(m), s(s), m_soft(soft_constraints), m_weights(weights) + m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_cancel(false) { m_assignment.resize(m_soft.size(), false); } @@ -413,6 +414,9 @@ namespace opt { } while (l_true == is_sat) { is_sat = s.check_sat_core(0,0); + if (m_cancel) { + is_sat = l_undef; + } if (is_sat == l_true) { if (wth.is_optimal()) { s.get_model(m_model); @@ -473,7 +477,7 @@ namespace opt { return m_imp->m_assignment[idx]; } void wmaxsmt::set_cancel(bool f) { - // no-op + m_imp->m_cancel = f; } void wmaxsmt::collect_statistics(statistics& st) const { // no-op diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index f282b47c3..3b9ed85cc 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -76,21 +76,54 @@ namespace smt { } // sort and coalesce arguments: std::sort(args.begin(), args.end()); - for (unsigned i = 0; i + 1 < size(); ++i) { - if (lit(i) == args[i+1].first) { - args[i].second += coeff(i+1); - for (unsigned j = i+1; j + 1 < size(); ++j) { - args[j] = args[j+1]; - } - args.pop_back(); + + unsigned i = 0, j = 1; + for (; j < size(); ++i) { + SASSERT(j > i); + literal l = lit(i); + for (; j < size() && lit(j) == lit(i); ++j) { + args[i].second += coeff(j); } - if (coeff(i).is_zero()) { - for (unsigned j = i; j + 1 < size(); ++j) { - args[j] = args[j+1]; - } - args.pop_back(); + if (j < size()) { + args[i+1].first = lit(j); + args[i+1].second = coeff(j); + ++j; } - } + } + if (i + 1 < size()) { + args.resize(i+1); + } + } + + void theory_pb::ineq::prune() { + numeral& k = m_k; + arg_t& args = m_args; + numeral nlt(0); + unsigned occ = 0; + for (unsigned i = 0; nlt < k && i < size(); ++i) { + if (coeff(i) < k) { + nlt += coeff(i); + ++occ; + } + } + if (0 < occ && nlt < k) { + IF_VERBOSE(2, verbose_stream() << "prune\n"; + for (unsigned i = 0; i < size(); ++i) { + verbose_stream() << coeff(i) << "*" << lit(i) << " "; + } + verbose_stream() << " >= " << k << "\n"; + ); + + for (unsigned i = 0; i < size(); ++i) { + if (coeff(i) < k) { + args[i] = args.back(); + args.pop_back(); + --i; + } + } + normalize(); + + } } lbool theory_pb::ineq::normalize() { @@ -121,20 +154,28 @@ namespace smt { // detect tautologies: if (k <= numeral::zero()) { args.reset(); + k = numeral::zero(); return l_true; } // detect infeasible constraints: if (sum < k) { args.reset(); + k = numeral::one(); return l_false; } - // normalize to integers. - numeral d(denominator(k)); - for (unsigned i = 0; i < size(); ++i) { - d = lcm(d, denominator(coeff(i))); + bool all_int = true; + for (unsigned i = 0; all_int && i < size(); ++i) { + all_int = coeff(i).is_int(); } - if (!d.is_one()) { + + if (!all_int) { + // normalize to integers. + numeral d(denominator(k)); + for (unsigned i = 0; i < size(); ++i) { + d = lcm(d, denominator(coeff(i))); + } + SASSERT(!d.is_one()); k *= d; for (unsigned i = 0; i < size(); ++i) { args[i].second *= d; @@ -182,6 +223,13 @@ namespace smt { k = numeral::one(); } else if (g > numeral::one()) { + IF_VERBOSE(2, verbose_stream() << "cut " << g << "\n"; + for (unsigned i = 0; i < size(); ++i) { + verbose_stream() << coeff(i) << "*" << lit(i) << " "; + } + verbose_stream() << " >= " << k << "\n"; + ); + // // Example 5x + 5y + 2z + 2u >= 5 // becomes 3x + 3y + z + u >= 3 @@ -226,6 +274,13 @@ namespace smt { numeral n1 = floor(n0); numeral n2 = ceil(k/min) - numeral::one(); if (n1 == n2 && !n0.is_int()) { + IF_VERBOSE(2, verbose_stream() << "set cardinality\n"; + for (unsigned i = 0; i < size(); ++i) { + verbose_stream() << coeff(i) << "*" << lit(i) << " "; + } + verbose_stream() << " >= " << k << "\n"; + ); + for (unsigned i = 0; i < size(); ++i) { args[i].second = numeral::one(); } @@ -300,6 +355,8 @@ namespace smt { bool_var abv = ctx.mk_bool_var(atom); ctx.set_var_theory(abv, get_id()); + IF_VERBOSE(3, verbose_stream() << mk_pp(atom, m) << "\n";); + ineq* c = alloc(ineq, literal(abv)); c->m_k = m_util.get_k(atom); numeral& k = c->m_k; @@ -324,7 +381,9 @@ namespace smt { } c->unique(); lbool is_true = c->normalize(); + c->prune(); + literal lit(abv); switch(is_true) { case l_false: @@ -339,7 +398,9 @@ namespace smt { break; } - // TBD: special cases: args.size() == 1 + // TBD: special cases: k == 1, or args.size() == 1 + + // maximal coefficient: numeral& max_watch = c->m_max_watch; @@ -983,14 +1044,12 @@ namespace smt { tout << "\n"; display(tout, c, true);); - if ((c.m_num_propagations & 0xF) == 0) { + if (true || (c.m_num_propagations & 0xF) == 0) { resolve_conflict(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(), lits.size(), lits.c_ptr()); - verbose_stream() << "\n";); } @@ -1031,7 +1090,7 @@ namespace smt { if (ctx.get_assignment(l) != l_false) { m_lemma.m_k -= coeff; - if (false && is_marked(v)) { + if (true && false && is_marked(v)) { SASSERT(ctx.get_assignment(l) == l_true); numeral& lcoeff = m_lemma.m_args[m_conseq_index[v]].second; lcoeff -= coeff; @@ -1173,6 +1232,7 @@ namespace smt { // It is not a correctness bug but causes to miss lemmas. // IF_VERBOSE(1, display_resolved_lemma(verbose_stream());); + TRACE("pb", display_resolved_lemma(tout);); return false; } @@ -1254,11 +1314,15 @@ namespace smt { } display(tout << "=> ", m_lemma);); + // 3x + 3y + z + u >= 4 + // ~x /\ ~y => z + u >= + + IF_VERBOSE(2, display(verbose_stream() << "lemma1: ", m_lemma);); hoist_maximal_values(); - lbool is_true = m_lemma.normalize(); + m_lemma.prune(); - IF_VERBOSE(2, display(verbose_stream() << "lemma: ", m_lemma);); + IF_VERBOSE(2, display(verbose_stream() << "lemma2: ", m_lemma);); switch(is_true) { case l_true: UNREACHABLE(); @@ -1290,7 +1354,7 @@ namespace smt { void theory_pb::hoist_maximal_values() { for (unsigned i = 0; i < m_lemma.size(); ++i) { - if (m_lemma.coeff(i) == m_lemma.k()) { + if (m_lemma.coeff(i) >= m_lemma.k()) { m_ineq_literals.push_back(~m_lemma.lit(i)); std::swap(m_lemma.m_args[i], m_lemma.m_args[m_lemma.size()-1]); m_lemma.m_args.pop_back(); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 81f3229aa..9a4c18ed4 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -92,6 +92,8 @@ namespace smt { void unique(); + void prune(); + bool well_formed() const; app_ref to_expr(context& ctx, ast_manager& m); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index f5ae23b07..c6c49ec5b 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -211,6 +211,9 @@ public: else if (a.is_mul(x, z, y) && is_numeral(y, r)) { ok = get_pb_sum(z, r*mul, args, coeffs, coeff); } + else if (a.is_to_real(x, y)) { + ok = get_pb_sum(y, mul, args, coeffs, coeff); + } else if (m.is_ite(x, y, z, u) && is_numeral(z, r) && is_numeral(u, q)) { insert_arg(r*mul, y, args, coeffs, coeff); // q*(1-y) = -q*y + q @@ -235,6 +238,9 @@ public: r.neg(); return true; } + if (a.is_to_real(e, e)) { + return is_numeral(e, r); + } return a.is_numeral(e, r); }