如何循环 Z3 变量以在 python 中添加约束答案

【问题标题】：How to loop a Z3 variable for adding constraints in python如何循环 Z3 变量以在 python 中添加约束
【发布时间】：2022-01-28 01:52:07
【问题描述】：

我想循环一个 Z3 变量以在 python 中添加约束。以下代码 sn-p 可能有助于澄清我面临的问题。

from z3 import *

a = Int('a')
b = [Int( 'b_' + str(i)) for i in range(10)]

s = Solver()
s.add(a <= 4)

for i in range(a): ################## How to do this? #####################
    s.add(b[i] == 1)

s.check()
s.model()

【问题讨论】：

可能将 range(a) 更改为 range(4) 或类似的，因为 a 是 z3 Int 对象
这是一个例子。假设 a 的值事先不知道。感谢您的评论。为了清楚起见，让我重新表述一下这个问题。
此时会解决a 吗？
变量需要通过其他约束来解决。每个约束都应该在一个求解器中。有依赖关系。因此顺序求解是不可能的。我有一个非常复杂的问题版本。我没有尝试做一个简化的表示。

标签： python z3 smt z3py

【解决方案1】：

你不能。这就是符号变量的全部意义所在。它的值可以是任何东西（当然，受制于你所设置的约束），因此它不能作为参数传递给range。

由于您的b 来自一个列表，您应该改为遍历该范围。比如：

for i in range(10):
  s.add(Implies(i < a,  b[i] == 1))

当然，这完全取决于您要达到的目标。您的问题听起来像是XY problem 的一个实例。如果您询问您想要实现的目标，而不是如何为符号变量模拟 range，您可能会得到更好的答案。

【讨论】：

很好的答案。在很多情况下，我已经解决了这样的问题。在以下情况下该怎么办？暗示（条件1，对于范围内的i（a）：条件2）
很高兴它有帮助。请参阅stackoverflow.com/help/someone-answers 了解您可以对此答案采取的措施；接受答案可以帮助将来可能遇到类似问题的其他人。
如果您有新问题，请单独提出。（即，创建一个新问题。）评论应该仅用于小评论/澄清。
问题尚未解决。场景怎么样：Implies(condition1,for i in range(a): condition2)
正如我所提到的；要么“编辑”您的问题以添加新变体；或开始一个新问题。（后者更好，因为包含许多不同子问题的问题通常会让读者和试图回答这些问题的人感到困惑。）评论不太适合进一步讨论。