mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix #5829
This commit is contained in:
parent
4f6fcf8ea7
commit
07d02ea415
|
@ -8883,7 +8883,7 @@ def _pb_args_coeffs(args, default_ctx=None):
|
|||
for i in range(len(coeffs)):
|
||||
_z3_check_cint_overflow(coeffs[i], "coefficient")
|
||||
_coeffs[i] = coeffs[i]
|
||||
return ctx, sz, _args, _coeffs
|
||||
return ctx, sz, _args, _coeffs, args
|
||||
|
||||
|
||||
def PbLe(args, k):
|
||||
|
@ -8893,7 +8893,7 @@ def PbLe(args, k):
|
|||
>>> f = PbLe(((a,1),(b,3),(c,2)), 3)
|
||||
"""
|
||||
_z3_check_cint_overflow(k, "k")
|
||||
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
|
||||
ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
|
||||
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
|
||||
|
||||
|
||||
|
@ -8904,7 +8904,7 @@ def PbGe(args, k):
|
|||
>>> f = PbGe(((a,1),(b,3),(c,2)), 3)
|
||||
"""
|
||||
_z3_check_cint_overflow(k, "k")
|
||||
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
|
||||
ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
|
||||
return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
|
||||
|
||||
|
||||
|
@ -8915,7 +8915,7 @@ def PbEq(args, k, ctx=None):
|
|||
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
|
||||
"""
|
||||
_z3_check_cint_overflow(k, "k")
|
||||
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
|
||||
ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
|
||||
return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
|
||||
|
||||
|
||||
|
|
|
@ -33,11 +33,9 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
unsigned arity, sort * const * domain, sort * range) {
|
||||
SASSERT(m_manager);
|
||||
ast_manager& m = *m_manager;
|
||||
for (unsigned i = 0; i < arity; ++i) {
|
||||
if (!m.is_bool(domain[i])) {
|
||||
for (unsigned i = 0; i < arity; ++i)
|
||||
if (!m.is_bool(domain[i]))
|
||||
m.raise_exception("invalid non-Boolean sort applied to 'at-most'");
|
||||
}
|
||||
}
|
||||
symbol sym;
|
||||
switch(k) {
|
||||
case OP_AT_LEAST_K: sym = m_at_least_sym; break;
|
||||
|
@ -50,9 +48,8 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
switch(k) {
|
||||
case OP_AT_LEAST_K:
|
||||
case OP_AT_MOST_K: {
|
||||
if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
|
||||
if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0)
|
||||
m.raise_exception("function expects one non-negative integer parameter");
|
||||
}
|
||||
func_decl_info info(m_family_id, k, 1, parameters);
|
||||
return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue