Неожиданное неизвестное с плохо определенной аксиомой определения функции - PullRequest
Новая
       6

Неожиданное неизвестное с плохо определенной аксиомой определения функции

0 голосов
/ 09 мая 2018

Программа SMT далее кодирует (плохо определенную) определение функции ∀ s · wild(s) = 1 + wild(s) немного окольным путем (применяя кодирование Дафни "ограниченных функций" рекурсивных функций), а затем пытается доказать, что wild(emp) = 1 + wild(emp). Однако Z3 4.6.0 (а также недавняя ночная версия 4.7.0) неожиданно дают unknown вместо unsat. 

(set-option :auto_config false) ;; true -> no change in behaviour
(set-option :smt.mbqi false) ;; true -> no change in behaviour

(declare-sort Snap)      ;; In the full example, this is ...
(declare-const emp Snap) ;; ... declared using declare-datatypes

(declare-fun wild (Snap) Int)
(declare-fun wild%limited (Snap) Int)

(assert (forall ((s Snap)) (! ;; AX-1
  (= (wild%limited s) (wild s))
  :pattern ((wild s))
)))

(assert (forall ((s Snap)) (! ;; AX-2
  (=
    (wild s)
    (+ 1 (wild%limited emp)))
  :pattern ((wild s))
)))

(push) ;; Full examples uses incremental mode
(assert
  (not 
    (= 
      (wild emp)
      (+ 1 (wild emp)))))
(check-sat) ;; UNKNOWN --- but why?
(pop)

Учитывая мое понимание Z3 и триггеров, я ожидаю, что произойдут следующие шаги доказательства: 

  ¬(wild(emp) = 1 + wild(emp))  // Source assertion
≡ ¬(1 + wild%limited(emp) = 1 + wild(emp))  // By AX-2
≡ ¬(1 + wild%limited(emp) = 1 + wild%limited(emp))  // By AX-1
≡ ¬(true)  // Done: UNSAT

Но этого не происходит. Я предполагаю, что аксиомы не созданы - и, действительно, get-info :all-statistics не сообщает количественно.

Кто-нибудь может пролить свет на это?

1 Ответ

0 голосов
/ 09 мая 2018

последнее утверждение упрощается до "true", поэтому не существует наземного вхождения (wild emp), который бы инициировал создание экземпляра квантора.

...