mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
address ubuntu warning and add shortcuts for maxsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
186afe7d10
commit
e3f0aff318
|
@ -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)
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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++;
|
||||
|
|
Loading…
Reference in a new issue