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

Поясню свой вопрос на примере:

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

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

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

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

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

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

Спасибо, --Иштиак


z3
person Ishtiaque Hussain    schedule 06.02.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

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

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

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

person Jeff    schedule 06.02.2012