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

【问题标题】：How to add a constraint which requires an integer variable belongs to an array?如何添加要求整数变量属于数组的约束？
【发布时间】：2018-06-23 14:48:05
【问题描述】：

假设我有一个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())

【问题讨论】：

我不明白这个问题。
这看起来不像您的代码功能的完整示例：您认为需要使用数字列表而不是使用 solve 和充分定义的 @987654331 @ 和 > 约束？
@timgeb “z3”和“z3py”标签在这里相当重要。 ericpony.github.io/z3py-tutorial/guide-examples.htm
@Mike'Pomax'Kamermans 啊，感谢您指出这一点！
什么是s？在s.add(x in a)

标签： python z3 smt z3py

【解决方案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

【讨论】：

【解决方案2】：

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

【讨论】：

【解决方案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]

【讨论】：