несколько ограничений в z3py, если условно

Question

Предположим, у нас есть 2 функции (funcA и funcB), которые создают некоторые ограничения в текущем контексте Z3.

Я хочу защитить их в блоке Z3 if.В z3py вы должны написать:

t = If(some_condition, funcA(), funcB())

Это зависит от того факта, что funcA и funcB возвращают некоторое выражение z3.Что если я захочу представить их как вызов функции, которая строит кучу ограничений, а не возвращает выражение, что может быть проще для этого?

Answer 1

Я бы превратил их в (псевдо-код):

for c in funcA():
   s.add(Implies(some_condition, c))

for c in funcB():
   s.add(Implies(Not(some_condition), c))