Переписать код в Z3 с квантификаторами
Парни
Я пишу модель, используя Microsft Z3, и мне нужно добавить следующие утверждения:
(declare-const line (Array Int Int))
(assert (and (> (select line 1) 0) (< (select line 1) 4)))
(assert (and (> (select line 2) 0) (< (select line 2) 4)))
(assert (and (> (select line 3) 0) (< (select line 3) 4)))
Как вы можете видеть, я пытаюсь заявить, что мой массив из 3 длин, называемый line, может иметь только элементы в [1..3]. Этот код работает отлично, однако я хотел бы иметь возможность сделать эти утверждения только с помощью строки кода, используя квантификаторы. Я пробовал:
(assert (forall ((i Int)) (=> (and (> i 0) (< i 4)) (and (> (select line i) 0) (< (select line i) 4)))))
Который я хотя бы работал... но после выполнения Z3 вернул unsat, чего не было с предыдущей версией кода.
Почему это происходит?
Это возможно?