如果有条件，z3py 中的多个约束

【问题标题】：multiple constraints in z3py if conditional如果有条件，z3py 中的多个约束
【发布时间】：2019-06-07 18:47:06
【问题描述】：

假设我们有 2 个函数（funcA 和 funcB）在 Z3 的当前上下文中构建一些约束。

我想保护 Z3 中的那些 if 块。在 z3py 中，你会写：

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

这取决于funcA 和funcB 返回一些z3 表达式这一事实。如果我想将它们表示为构建一堆约束而不是返回表达式的函数调用怎么办，有什么更简单的方法来做到这一点？

【问题讨论】：

标签： z3 z3py

【解决方案1】：

我会把它们变成（伪代码）：

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

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

【讨论】：

啊，我明白了，你在这里做什么。我可以改变 funcA 和 funcB 来实现这个含义。但是有没有更好的方法从函数中获取约束列表（就像你在这个伪代码中所做的那样）
如果您将约束实现为布尔值，那么您可以轻松地做到这一点。如果您的函数funcA/funcB 实际上执行了s.add 调用，那么恐怕您就不走运了。您应该将它们改回以返回布尔值。（或者你可以让他们把some_condition作为参数，在内部做正确的事情。）