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

Question

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

添加约束

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

谢谢！

这是我使用的 python 代码。我认为输出答案是 s 是可满足的，因为 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

Answer 2

"x in a" 是一个 python 表达式，在断言约束之前计算结果为 False，因为变量 x 不属于数组。

Answer 3

一种方法是使用循环

构建 z3.And 或 z3.Or 约束

# Finds all numbers in the domain, for which it's square is also in the domain

import z3
exclude = [1,2]
domain  = list(range(128))
number  = z3.Int('number')
squared = number * number
solver  = z3.Solver()
solver.add(z3.Or([  number  == value for value in domain  ]))
solver.add(z3.Or([  squared == value for value in domain  ]))
solver.add(z3.And([ number  != value for value in exclude ]))
solver.add(z3.And([ squared != value for value in exclude ]))
solver.push()  # create stack savepoint

output = []
while solver.check() == z3.sat:
  value = solver.model()[number].as_long()
  solver.add( number != value )
  output.append(value)

solver.pop()  # reset stack to last solver.push()

print(output)
# [10, 0, 4, 6, 5, 11, 9, 8, 3, 7]

print(sorted(output))
# [0, 3, 4, 5, 6, 7, 8, 9, 10, 11]

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

How to add a constraint which requires an integer variable belongs to an array?

python

smt

z3

z3py