Как добавить ограничение, требующее, чтобы целочисленная переменная принадлежала массиву?

Question

Предположим, у меня есть z3py целочисленная переменная x = Int('x') и целочисленный массив a = [1, 2, 3].Затем я добавляю ограничение через s.add (x в 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

"x in a" - это выражение на языке python, которое оценивается как False до того, как вы утвердите ограничение, поскольку переменная x не принадлежит массиву.

Answer 2

Это должно сделать:

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