From 2646e0a1c0213ea89f54112a94cb65fa9572f3c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Jan 2021 12:17:35 -0800 Subject: [PATCH] have add_soft accept an interable of Booleans. --- src/api/python/z3/z3.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 57b4fd48b..4f4e4bee5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7490,6 +7490,11 @@ class Optimize(Z3PPObject): if id is None: id = "" id = to_symbol(id, self.ctx) + 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)