Почему Z3 возвращает Unknown для этих клаузул - PullRequest
Новая
       8

Почему Z3 возвращает Unknown для этих клаузул

0 голосов
/ 11 октября 2019

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

Я видел несколько примеров, в которых отрицание работает нормально. Например, 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)

Интересно, есть лиспособ переписать мои статьи в фрагмент клаузулы Horn из Z3.

...