mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

generator

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-25 19:18:55 -08:00
parent 4b6d7ca097
commit dccfecb488
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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."""