Квантор шаблонов в Z3 - PullRequest
Новая
       38

Квантор шаблонов в Z3

0 голосов
/ 15 мая 2019

У меня возникают проблемы при попытке доказать этот довольно простой запрос Z3. 

(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun sum (Int) Int)
(declare-fun list () (Array Int Int))
(declare-fun i0 () Int)
(declare-fun s0 () Int)
(declare-fun i1 () Int)
(declare-fun s1 () Int)
(assert (forall ((n Int))
  (! (or (not (<= n 0)) (= (sum n) 0)) 
     :pattern ((sum n)))))
(assert (forall ((n Int))
  (! (let ((a1 (= (sum n)
                   (+ (select list (- n 1))
                      (sum (- n 1))))))
       (or (<= n 0) a1))
     :pattern ((sum n)))))
(assert (>= i0 0))
(assert (= s0 (sum i0)))
(assert (= i1 (+ 1 i0)))
(assert (= s1 (+ 1 s0 (select list i0))))
(assert (not (= s1 (sum i1))))

(check-sat)

Мне кажется, что последнее утверждение должно создать экземпляр второго количественного выражения для i1, в то время как утверждение, включающее s0, должно создать экземпляры квантификаторов дляi0.Эти два должны легко привести к UNSAT.

Однако Z3 возвращает неизвестное.Чего мне не хватает?

1 Ответ

1 голос
/ 16 мая 2019

Не берите в голову, в моем запросе произошла глупая ошибка.

Этот код: 

(assert (= s1 (+ 1 s0 (select list i0))))

должен был быть: 

(assert (= s1 (+ s0 (select list i0))))
...