From e3f0aff318b5873cfe858191b8e73ed716405b59 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Oct 2016 16:22:13 -0700 Subject: [PATCH] address ubuntu warning and add shortcuts for maxsat Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 17 ++++++------ src/ast/rewriter/bv_bounds.cpp | 2 +- src/opt/maxsmt.cpp | 6 ++-- src/tactic/arith/card2bv_tactic.cpp | 40 +++++++++++++++++++++++++++ src/tactic/arith/card2bv_tactic.h | 2 ++ src/tactic/bv/bv_bound_chk_tactic.cpp | 1 - 6 files changed, 56 insertions(+), 12 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5c677c4f3..c360a9bdc 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7548,11 +7548,11 @@ def Sum(*args): a__0 + a__1 + a__2 + a__3 + a__4 """ args = _get_args(args) - if __debug__: - _z3_assert(len(args) > 0, "Non empty list of arguments expected") + if len(args) == 0: + return 0 ctx = _ctx_from_ast_arg_list(args) - if __debug__: - _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") + if ctx is None: + return _reduce(lambda a, b: a + b, args, 0) args = _coerce_expr_list(args, ctx) if is_bv(args[0]): return _reduce(lambda a, b: a + b, args, 0) @@ -7560,6 +7560,7 @@ def Sum(*args): _args, sz = _to_ast_array(args) return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx) + def Product(*args): """Create the product of the Z3 expressions. @@ -7573,11 +7574,11 @@ def Product(*args): a__0*a__1*a__2*a__3*a__4 """ args = _get_args(args) - if __debug__: - _z3_assert(len(args) > 0, "Non empty list of arguments expected") + if len(args) == 0: + return 1 ctx = _ctx_from_ast_arg_list(args) - if __debug__: - _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression") + if ctx is None: + return _reduce(lambda a, b: a * b, args, 1) args = _coerce_expr_list(args, ctx) if is_bv(args[0]): return _reduce(lambda a, b: a * b, args, 1) diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp index 0f82a85c9..22decbb7c 100644 --- a/src/ast/rewriter/bv_bounds.cpp +++ b/src/ast/rewriter/bv_bounds.cpp @@ -92,7 +92,7 @@ bool bv_bounds::is_uleq(expr * e, expr * & v, numeral & c) { expr * const ulel0 = to_app(ulel)->get_arg(0); if (ulel0 != eql0) return false; if ((m_bv_util.get_extract_high(ulel) + 1) != m_bv_util.get_extract_low(eql)) return false; - if (!m_bv_util.get_extract_low(ulel) == 0) return false; + if (m_bv_util.get_extract_low(ulel) != 0) return false; if (!m_bv_util.is_numeral(uler, uleqr_val, uleqr_sz)) return false; SASSERT(m_bv_util.get_bv_size(ulel0) == uleqr_sz + eqr_sz); v = ulel0; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 1ad2a09be..fa4897046 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -267,8 +267,10 @@ namespace opt { void maxsmt::display_answer(std::ostream& out) const { for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { - out << mk_pp(m_soft_constraints[i], m) - << (get_assignment(i)?" |-> true\n":" |-> false\n"); + expr* e = m_soft_constraints[i]; + bool is_not = m.is_not(e, e); + out << mk_pp(e, m) + << ((is_not != get_assignment(i))?" |-> true\n":" |-> false\n"); } } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 7d7097958..2b551229d 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -116,6 +116,9 @@ namespace pb { result = m.mk_and(sz, args); return BR_DONE; } + if (is_atmost1(f, sz, args, result)) { + return BR_DONE; + } br_status st = mk_shannon(f, sz, args, result); if (st == BR_FAILED) { mk_bv(f, sz, args, result); @@ -165,6 +168,43 @@ namespace pb { return BR_FAILED; } + expr_ref card2bv_rewriter::mk_atmost1(unsigned sz, expr * const* args) { + expr_ref f1(m), f2(m), f3(m), result(m); + f1 = bv.mk_bv(sz, args); + f2 = bv.mk_bv_sub(f1, bv.mk_numeral(rational(1), sz)); + f3 = m.mk_app(bv.get_fid(), OP_BAND, f1, f2); + result = m.mk_eq(f3, bv.mk_numeral(rational(0), sz)); + return result; + } + + bool card2bv_rewriter::is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result) { + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + if (pb.get_k(f).is_one() && pb.has_unit_coefficients(f)) { + result = mk_atmost1(sz, args); + return true; + } + return false; + case OP_AT_LEAST_K: + case OP_PB_GE: + if (pb.get_k(f) == rational(sz-1) && pb.has_unit_coefficients(f)) { + expr_ref_vector nargs(m); + for (unsigned i = 0; i < sz; ++i) { + nargs.push_back(mk_not(args[i])); + } + result = mk_atmost1(nargs.size(), nargs.c_ptr()); + return true; + } + return false; + case OP_PB_EQ: + return false; + default: + UNREACHABLE(); + return false; + } + } + bool card2bv_rewriter::is_or(func_decl* f) { switch (f->get_decl_kind()) { case OP_AT_MOST_K: diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h index 30a91416d..91ed68969 100644 --- a/src/tactic/arith/card2bv_tactic.h +++ b/src/tactic/arith/card2bv_tactic.h @@ -52,6 +52,8 @@ namespace pb { expr* mk_ite(expr* c, expr* hi, expr* lo); bool is_or(func_decl* f); bool is_and(func_decl* f); + bool is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result); + expr_ref mk_atmost1(unsigned sz, expr * const* args); public: card2bv_rewriter(ast_manager& m); diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index c3f32aaaf..1b90e05b1 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -71,7 +71,6 @@ struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg { result_pr = 0; const family_id fid = f->get_family_id(); if (fid != m_b_rw.get_fid()) return BR_FAILED; - const decl_kind k = f->get_decl_kind(); bv_bounds bvb(m()); const br_status rv = bvb.rewrite(m_bv_ineq_consistency_test_max, f, num, args, result); if (rv != BR_FAILED && (m_m.is_false(result) || m_m.is_true(result))) m_stats.m_unsats++;