mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

have add_soft accept an interable of Booleans.

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-25 12:17:35 -08:00
parent 7d60d8462d
commit 2646e0a1c0
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -7490,6 +7490,11 @@ class Optimize(Z3PPObject):
if id is None: if id is None:
id = "" id = ""
id = to_symbol(id, self.ctx) 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) v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
return OptimizeObjective(self, v, False) return OptimizeObjective(self, v, False)