python - 如何添加需要整数变量属于数组的约束？

Question

假设我有一个 z3py整型变量 x = Int('x')，和一个整型数组 a = [1, 2, 3]。然后我通过 s.add(x in a) 添加约束。

我认为这是可满足的，因为 x 可以是 1 或 2 或 3。但实际上是不可满足的。谁能告诉我如何添加约束以确保 x in a？

谢谢!

这是我使用的 python 代码。我认为输出答案是 s is satisfiable，因为 x 可以等于 1 或 2 或 3，那么约束 x in a 就满足了。但答案实际上并不令人满意。也许这不是指定此约束的正确方法。所以我的问题是如何指定这样的约束以确保变量只能用特定数组中的值实例化。

from z3 import *
x = Int('x')

a = [1, 2, 3]

s = Solver()

s.add(x in a)

print(s.check())

Answer 1

应该这样做:

from z3 import *

a = [1,2,3]

s = Solver()
x = Int('x')
s.add(Or([x == i for i in a]))

# Enumerate all possible solutions:
while True:
    r = s.check()
    if r == sat:
        m = s.model()
        print m
        s.add(x != m[x])
    else:
        print r
        break

当我运行它时，我得到:

[x = 1]
[x = 2]
[x = 3]
unsat