From b82b53dc349cf90b522983d3d03afec1d1a85167 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Oct 2016 17:41:52 -0700 Subject: [PATCH] add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 4 + src/ast/rewriter/pb2bv_rewriter.cpp | 162 ++++++++++++++++++------ src/tactic/portfolio/enum2bv_solver.cpp | 2 - 3 files changed, 125 insertions(+), 43 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 4f0379674..410c50852 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -264,6 +264,10 @@ public: bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); } bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); } bool is_gt(expr const * n) const { return is_app_of(n, m_afid, OP_GT); } + bool is_le(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LE); } + bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); } + bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); } + bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); } bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); } bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); } bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); } diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 48d566f11..5cd7789ff 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -79,6 +79,9 @@ struct pb2bv_rewriter::imp { pb_util pb; bv_util bv; expr_ref_vector m_trail; + expr_ref_vector m_args; + rational m_k; + vector m_coeffs; template expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) { @@ -109,8 +112,22 @@ struct pb2bv_rewriter::imp { // The procedure for checking >= k is symmetric and checking for = k is // achieved by checking <= k on intermediary addends and the resulting sum is = k. // + // is_le = l_true - <= + // is_le = l_undef - = + // is_le = l_false - >= + // template - expr_ref mk_le_ge(func_decl *f, unsigned sz, expr * const* args, rational const & k) { + expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) { + TRACE("pb", + for (unsigned i = 0; i < sz; ++i) { + tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " "; + } + switch (is_le) { + case l_true: tout << "<= "; break; + case l_undef: tout << "= "; break; + case l_false: tout << ">= "; break; + } + tout << m_k << "\n";); if (k.is_zero()) { if (is_le != l_false) { return expr_ref(m.mk_not(mk_or(m, sz, args)), m); @@ -119,6 +136,9 @@ struct pb2bv_rewriter::imp { return expr_ref(m.mk_true(), m); } } + if (k.is_neg()) { + return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m); + } SASSERT(k.is_pos()); expr_ref zero(m), bound(m); expr_ref_vector es(m), fmls(m); @@ -126,7 +146,8 @@ struct pb2bv_rewriter::imp { zero = bv.mk_numeral(rational(0), nb); bound = bv.mk_numeral(k, nb); for (unsigned i = 0; i < sz; ++i) { - if (pb.get_coeff(f, i) > k) { + SASSERT(!m_coeffs[i].is_neg()); + if (m_coeffs[i] > k) { if (is_le != l_false) { fmls.push_back(m.mk_not(args[i])); } @@ -135,7 +156,7 @@ struct pb2bv_rewriter::imp { } } else { - es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), nb), zero)); + es.push_back(mk_ite(args[i], bv.mk_numeral(m_coeffs[i], nb), zero)); } } while (es.size() > 1) { @@ -165,6 +186,10 @@ struct pb2bv_rewriter::imp { expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) { decl_kind kind = f->get_decl_kind(); rational k = pb.get_k(f); + m_coeffs.reset(); + for (unsigned i = 0; i < sz; ++i) { + m_coeffs.push_back(pb.get_coeff(f, i)); + } SASSERT(!k.is_neg()); switch (kind) { case OP_PB_GE: @@ -173,13 +198,13 @@ struct pb2bv_rewriter::imp { nargs.append(sz, args); dualize(f, nargs, k); SASSERT(!k.is_neg()); - return mk_le_ge(f, sz, nargs.c_ptr(), k); + return mk_le_ge(sz, nargs.c_ptr(), k); } case OP_PB_LE: case OP_AT_MOST_K: - return mk_le_ge(f, sz, args, k); + return mk_le_ge(sz, args, k); case OP_PB_EQ: - return mk_le_ge(f, sz, args, k); + return mk_le_ge(sz, args, k); default: UNREACHABLE(); return expr_ref(m.mk_true(), m); @@ -228,7 +253,6 @@ struct pb2bv_rewriter::imp { } } - public: card2bv_rewriter(imp& i, ast_manager& m): @@ -238,7 +262,8 @@ struct pb2bv_rewriter::imp { pb(m), bv(m), m_sort(*this), - m_trail(m) + m_trail(m), + m_args(m) {} br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { @@ -247,8 +272,31 @@ struct pb2bv_rewriter::imp { ++m_imp.m_num_translated; return BR_DONE; } - else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) { + else if (au.is_le(f) && is_pb(args[0], args[1])) { ++m_imp.m_num_translated; + result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + return BR_DONE; + } + else if (au.is_lt(f) && is_pb(args[0], args[1])) { + ++m_imp.m_num_translated; + ++m_k; + result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + return BR_DONE; + } + else if (au.is_ge(f) && is_pb(args[1], args[0])) { + ++m_imp.m_num_translated; + result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + return BR_DONE; + } + else if (au.is_gt(f) && is_pb(args[1], args[0])) { + ++m_imp.m_num_translated; + ++m_k; + result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); + return BR_DONE; + } + else if (m.is_eq(f) && is_pb(args[0], args[1])) { + ++m_imp.m_num_translated; + result = mk_le_ge(m_args.size(), m_args.c_ptr(), m_k); return BR_DONE; } else { @@ -256,43 +304,75 @@ struct pb2bv_rewriter::imp { } } - // - // NSB: review - // we should remove this code and rely on a layer above to deal with - // whatever it accomplishes. It seems to break types. - // - bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - if (f->get_decl_kind() == OP_ADD) { - unsigned bits = 0; - for (unsigned i = 0; i < sz; i++) { - rational val1, val2; - if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) { - bits += val1.get_num_bits(); + bool is_pb(expr* x, expr* y) { + m_args.reset(); + m_coeffs.reset(); + m_k.reset(); + return is_pb(x, rational::one()) && is_pb(y, rational::minus_one()); + } + + bool is_pb(expr* e, rational const& mul) { + if (!is_app(e)) { + return false; + } + app* a = to_app(e); + rational r, r1, r2; + expr* c, *th, *el; + unsigned sz = a->get_num_args(); + if (a->get_family_id() == au.get_family_id()) { + switch (a->get_decl_kind()) { + case OP_ADD: + for (unsigned i = 0; i < sz; ++i) { + if (!is_pb(a->get_arg(i), mul)) return false; } - else if (m.is_ite(args[i]) && - au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() && - au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) { - bits++; + return true; + case OP_SUB: { + if (!is_pb(a->get_arg(0), mul)) return false; + r = -mul; + for (unsigned i = 1; i < sz; ++i) { + if (!is_pb(a->get_arg(1), r)) return false; } - else - return false; + return true; + } + case OP_UMINUS: + return is_pb(a->get_arg(0), -mul); + case OP_NUM: + VERIFY(au.is_numeral(a, r)); + m_k += mul * r; + return true; + case OP_MUL: + if (sz != 2) { + return false; + } + if (au.is_numeral(a->get_arg(0), r)) { + r *= mul; + return is_pb(a->get_arg(1), r); + } + if (au.is_numeral(a->get_arg(1), r)) { + r *= mul; + return is_pb(a->get_arg(0), r); + } + return false; + default: + return false; + } + } + if (m.is_ite(a, c, th, el) && au.is_numeral(th, r1) && au.is_numeral(el, r2)) { + r1 *= mul; + r2 *= mul; + if (r1 < r2) { + m_args.push_back(::mk_not(m, c)); + m_coeffs.push_back(r2-r1); + m_k -= r1; + } + else { + m_args.push_back(c); + m_coeffs.push_back(r1-r2); + m_k -= r2; } - - result = 0; - for (unsigned i = 0; i < sz; i++) { - rational val1, val2; - expr * q; - if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) - q = bv.mk_numeral(val1, bits); - else - q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits)); - result = (i == 0) ? q : bv.mk_bv_add(result.get(), q); - } return true; } - else { - return false; - } + return false; } void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 369402114..b0f11cb91 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -115,8 +115,6 @@ public: } } lbool r = m_solver->get_consequences(asms, bvars, consequences); - std::cout << consequences.size() << "\n"; - // translate bit-vector consequences back to enumeration types for (unsigned i = 0; i < consequences.size(); ++i) {