mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

fix #7105

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-30 15:41:14 -08:00
parent 67e5ba9f79
commit 28c44a6ed0
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -9069,7 +9069,7 @@ def AtMost(*args):
def AtLeast(*args):
"""Create an at-most Pseudo-Boolean k constraint.
"""Create an at-least Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)

7
src/api/python/z3/z3printer.py
View file

@ -99,6 +99,7 @@ _z3_op_to_str = {
Z3_OP_ARRAY_EXT: "Ext",
Z3_OP_PB_AT_MOST: "AtMost",
Z3_OP_PB_AT_LEAST: "AtLeast",
Z3_OP_PB_LE: "PbLe",
Z3_OP_PB_GE: "PbGe",
Z3_OP_PB_EQ: "PbEq",
@ -1111,6 +1112,10 @@ class Formatter:
k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
def pp_atleast(self, a, d, f, xs):
k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
def pp_pbcmp(self, a, d, f, xs):
chs = a.children()
rchs = range(len(chs))
@ -1163,6 +1168,8 @@ class Formatter:
return self.pp_K(a, d, xs)
elif k == Z3_OP_PB_AT_MOST:
return self.pp_atmost(a, d, f, xs)
elif k == Z3_OP_PB_AT_LEAST:
return self.pp_atleast(a, d, f, xs)
elif k == Z3_OP_PB_LE:
return self.pp_pbcmp(a, d, f, xs)
elif k == Z3_OP_PB_GE: