Использование Array в логике HORN в Spacer/Z3

Question

Есть ли какой-нибудь способ использовать «неинтерпретируемые функции» (UIF) внутри запросов Horn?

Я думаю, вы используете UIF для представления «переменных Хорна», поэтому, возможно, я подумал, что могу подделать то, что хочу, с помощью массивов. Однако следующее не работает:

      (set-logic HORN)

(declare-fun k1 (Int) Bool)

(declare-const foo (Array Int Int))

(assert (forall ((v Int)) (=> (< 666 (select foo v)) (k1 v))))

(assert (forall ((v Int)) (=> (k1 v) (< 0 (select foo v)))))

(check-sat)

(get-model)

Есть ли способ заставить вышеизложенное работать? Спасибо!

Answer 1

@nikolaj-bjorner ответил на вопрос по электронной почте, позвольте мне опубликовать ответ здесь для других:

Пример отсутствует во фрагменте «HORN», который допускает неинтерпретируемые предикаты только на верхнем уровне. Другие символы должны иметь универсальную количественную оценку.

Ари (Гурфинкель) и его коллеги работают над расширениями, которые обрабатывают неинтерпретируемые функции на верхнем уровне.

Логически это четко определено: просто найдите решение для предикатов и функций, удовлетворяющих заданному набору формул.

Они опубликовали об этом в FMCAD и других местах.

Иногда мы используем формализации вида:

      (set-logic HORN)

(declare-fun k1 ((Array Int Int) Int) Bool)

(assert (forall ((v Int) (foo (Array Int Int)))) (=> (< 666 (select foo v)) (k1 foo v))))

(assert (forall ((v Int) (foo (Array Int Int))))) (=> (k1 foo v) (< 0 (select foo v)))))
 
(check-sat)
 
(get-model)