From dccfecb4882c4a06f002e8478b88ed08bdc4fe7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Jan 2021 19:18:55 -0800 Subject: [PATCH] generator Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 4f4e4bee5..0e87fdd42 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7490,13 +7490,12 @@ class Optimize(Z3PPObject): if id is None: id = "" id = to_symbol(id, self.ctx) + def asoft(a): + v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id) + return OptimizeObjective(self, v, False) if isinstance(arg, iterable): - for a in arg: - v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id) - yield OptimizeObjective(self, v, False) - return - v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id) - return OptimizeObjective(self, v, False) + return [asoft(a) for a in arg] + return asoft(arg) def maximize(self, arg): """Add objective function to maximize."""