Smt2-lib: почему я получаю разницу в поведении между `Declare-Const + Assert` и` define-fun`? - PullRequest
Новая
       30

Smt2-lib: почему я получаю разницу в поведении между `Declare-Const + Assert` и` define-fun`?

0 голосов
/ 14 февраля 2019

У меня есть модель z3, написанная в формате smt2-lib.Я заметил, что, когда я использую: 

(declare-const flat1 (Seq Dummy))
(assert (= flat1 (unroll dummyFormula1)))

Модель насыщена, в то время как при использовании: 

(define-fun flat1 () (Seq Dummy) (unroll dummyFormula1))

модель сообщается как неизвестная.Почему разница важна?Если это поможет, я могу создать минимальную версию моей модели.

Edit # 1 - минимальный пример

Обязательно запустите его, используя z3 из github master, потому чтоиз эта ошибка .Вы можете переключаться между двумя версиями, которые я указал с помощью A) и B) ниже. 

(set-option :produce-models true)

; --------------- Basic Definitions -------------------

(declare-datatype Dummy (A B))

(declare-datatype Formula
  ((Base (forB Dummy))
   (And  (andB1 Formula) (andB2 Formula))
   (Or   (orB1 Formula) (orB2 Formula))
   (Not  (notB Formula))))

(declare-const dummyFormula1 Formula)
(assert (= dummyFormula1 (Base A)))

(declare-const dummyFormula2 Formula)
(assert (= dummyFormula2 (And (Base A) (Base A))))

; --------------- Some functions -----------------------

(define-fun
  in_list ((o Dummy) (l (Seq Dummy))) Bool
  (seq.contains l (seq.unit o)))

(define-fun
  permutation ((l1 (Seq Dummy)) (l2 (Seq Dummy))) Bool
  (forall ((o Dummy)) (= (in_list o l1) (in_list o l2))))

(define-fun-rec unroll ((f Formula)) (Seq Dummy)
  (match f
    (((Base j)    (seq.unit j))
     ((And f1 f2) (seq.++ (unroll f1) (unroll f2)))
     ((Or  f1 f2) (seq.++ (unroll f1) (unroll f2)))
     ((Not f1)    (unroll f1)))))

; -------------- The question -------------------------

;; Here are two versions that should express the same idea, but try commenting
;; the first one and uncommenting the second one!

;; A)

(declare-const flat1 (Seq Dummy))
(assert (= flat1 (unroll dummyFormula1)))

;; B)

; (define-fun flat1 () (Seq Dummy) (unroll dummyFormula1))
; -----------------------------------------------------

(declare-const flat2 (Seq Dummy))
(assert (= flat2 (unroll dummyFormula2)))

(assert (permutation flat1 flat2))

; --------------- Verify -------------------
(check-sat)
(get-model)

1 Ответ

0 голосов
/ 14 февраля 2019

Трудно сказать, не глядя на внутренности z3.Но я хочу отметить, что хотя эти две конструкции очень похожи, между ними есть небольшая разница.

Если вы посмотрите на страницу 62 стандарта (http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf),, там написано: 

(define-fun f ((x1 σ1) · · · (xn σn)) σ t)

  with n ≥ 0 and t not containing f is semantically equivalent to the command sequence

(declare-fun f (σ1 · · · σn) σ)
(assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t)).

Итак, когда вы используете форму define-fun, вы явно вводите квантифицированную формулу. Когда вы используете declare-const / assert, как вы делали вручную, это количественное определение не существует.

Теперь вы можете утверждать, что не имеют параметров в вашем случае, поэтому не должно быть никакой разницы, и я бы с вами согласился. Но вы также используете совершенно новые функции, такие как match,define-fun-rec и т. Д., Поэтому очевидно, что z3 спотыкается о чем-то здесь. Так как у вас уже есть минимальный пример, почему бы не опубликовать его на сайте вопросов о github z3 и получить некоторую обратную связь там. Я подозреваю, что, возможно, макросоискатель пропускает случайи не может создать экземпляр этого конкретного случая, но на самом деле это трудно сказать, и для этого также может быть веская причина.

Если вы пишете там и получаете хороший ответ, обновите этот вопрос, чтобы мыТеперь, что происходит!

...