Smt2-lib：为什么我会在 `declare-const + assert` 和 `define-fun` 之间得到不同的行为？

Question

我有一个以 smt2-lib 格式编写的 z3 模型。我注意到当我使用时：

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

模型是坐着的，而当我使用时：

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

模型被报告为未知。 为什么差异很重要？如果有帮助，我可以生成模型的最小版本。

编辑 #1 - 一个最小的示例

由于this bug，请务必使用来自 github master 的 z3 运行它。您可以在下面我用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)

Answer 1

不看 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 在这里遇到了一些问题。既然您已经有了一个最小的示例，为什么不将它发布到 z3 github 问题站点并在那里获得一些反馈。我怀疑宏查找器可能缺少一个案例并且无法实例化这个特殊案例，但真的很难说，也可能有一个很好的理由。

如果您确实在那里发帖并得到了很好的答案，请更新此问题，以便我们知道发生了什么！