Почему Z3 возвращает Неизвестно для этих пунктов рога

Question

Я использую Z3, чтобы решить свои предложения рог. В теле предложений Horn неинтерпретированные предикаты должны быть положительными. Однако мне нужно отрицание некоторых неинтерпретированных предикатов.

Я видел несколько примеров, в которых отрицание работает нормально. Например, Z3 вернетsat для следующего примера:

(set-logic HORN)
(declare-fun inv (Int) Bool)

(assert (inv 0))
(assert (forall ((k Int)) (or (> k 10) (not (inv k)) (inv (+ k 1)))))
(check-sat)

Но мой пример выглядит следующим образом, для которого Z3 возвращает unknown.

(set-logic HORN)
(declare-fun inv (Int  ) Bool)
(declare-fun s ( Int ) Bool)

(assert (forall ((k Int) (pc Int))(=>(and  (= pc 1)(= k 0))  (inv k ))))

(assert (forall ((k Int)(k_p Int)(pc Int)(pc_p Int))
  (=>(and  (inv k )(= pc 1)(= pc_p 2)(= k_p (+ k 1))(not (s pc ))(s pc_p ))  
(inv  k_p ))))

(check-sat)

Интересно, есть ли способ переписать мои предложения во фрагмент предложения Хорна Z3.

Answer 1

Ваши предложения отсутствуют во фрагменте Horn, потому что предикат s используется с обеими полярностями в последнем утверждении. Итак, есть два вхождения предиката с положительной полярностью (оба (s pc) и (inv k_p) имеют положительную полярность). Основной способ избежать проблем с полярностью - ввести дополнительный аргумент для s типа Bool. Следовательно, вам также нужно будет сказать, какова спецификация s, используя предложения Horn, чтобы все это имело смысл. Типичный сценарий состоит в том, что s кодирует поведение рекурсивной процедуры, а дополнительный логический аргумент s будет возвращаемым значением процедуры s. Конечно, эта кодировка не гарантирует, что s является полным или функциональным. Есть второй подход, который заключается в добавлении дополнительного аргумента к "inv", где вы позволяете 's' быть массивом. Тогда вхождения (not (s pc)) становится (not (select s pc)),и т.д. Все зависит от цели вашей кодировки, что имеет смысл.