From 28c44a6ed0661a0f128bebc22d7d57eaab6ec390 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Jan 2024 15:41:14 -0800 Subject: [PATCH] fix #7105 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- src/api/python/z3/z3printer.py | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b3b4351ab..2f34b91f6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index df50aa9b9..2da5f89da 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -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: