Могу ли я указать решение или область поиска в Z3?

Question

Позвольте мне объяснить мой вопрос на примере:

Предположим, у меня есть область возможных дискретных целых чисел, например, -1, 0, 2, 3, 5 и 6. Теперь я ищу решение (или модель) для переменной x, которая будет удовлетворять следующим ограничениям:

(x> 0) && (x <6) && (x! = 3) && (x> 2)

Ответ будет (из области решения) = 5, верно?

Как я могу сделать это в Z3?

То есть я хотел бы определить пространство решений с использованием дискретных объектов, а затем установить несколько ограничений и попросить Z3 проверить на удовлетворительность. Если удовлетворительно, то хотите модель.

Может кто-нибудь помочь мне с примером?

Спасибо, --Ishtiaque

Answer 1

Утверждая, что x == -1 || x == 0 || x == 2 || x == 3 || x == 5 || x == 6 в качестве аксиомы, заранее должен это сделать. Я не знаю, есть ли в Z3 лучший способ.

Edit: Другим решением может быть использование массива, хотя я раньше не использовал их. Концептуально должно быть возможно объявить массив A, который содержит числа, и затем сказать:

(существует (y Int) (= (выберите A y) x)) `

Не уверен, что это точный синтаксис, так как я раньше не использовал массивы, но, надеюсь, он должен работать.