SMT-LIB代码报‘Symbol Z未声明’错误求助及版本适配疑问

问题描述 #

使用SMT-LIB 2.7语法编写了以下代码：

(set-option :print-success false)
(set-logic ALL)

(define-sort |Z| () Int)
(declare-sort P 1)
(define-sort |POW Z| () (P |Z|))

(declare-const vmax |Z|)
(declare-const vset |POW Z|)
(declare-const |set.empty Z| |POW Z|)

(assert (!
  (forall ((e |Z|))
    (not (|set.in |Z|| e |set.empty |Z||)))
  :named |ax.set.in.empty Z|))

(declare-fun |set.in Z| (|Z| |POW Z|) Bool)
(declare-fun max (|POW Z|) |Z|)

(assert (!
  (forall ((s |POW Z|))
    (=> (not (= s |set.empty |Z||))
        (|set.in |Z|| (max s) s)))
  :named |ax.max.is.member|))

(assert (!
  (forall ((s |POW Z|) (e |Z|))
    (=> (|set.in |Z|| e s)
        (<= e (max s))))
  :named |ax.max.is.ge|))

(assert (!
  (not (= vmax (max vset)))
  :named |Goal|))

(check-sat)
(exit)

使用CVC4 2.6版本求解器执行时，出现如下解析错误：

(error "Parse Error: output.smt:11.36: Symbol Z is not declared.
(forall ((e |Z|)) (not (|set.in |Z|| e |set.empty |Z||)))
                                     ^")

已通过(define-sort |Z| () Int)声明Z，但仍报错，怀疑是SMT-LIB版本不匹配（用2.7语法但用2.6求解器）导致，且找不到2.7兼容求解器。

错误原因分析 #

• 符号引用错误：核心问题是函数名的写法错误。你声明的函数是|set.in Z|，但在断言中错误地写成了|set.in |Z||。带竖线的符号是一个完整的标识符，|set.in |Z||会被解析为包含未声明符号Z的无效标识符，而非引用之前定义的|Z|排序。
• 版本兼容误解：CVC4 2.6对SMT-LIB 2.7的基础语法支持足够，本次错误并非由版本不匹配直接导致，而是符号使用不当。

修复后的代码 #

将所有错误的|set.in |Z||替换为正确的|set.in Z|，同时调整函数声明位置确保先声明再使用，修正后的代码如下：

(set-option :print-success false)
(set-logic ALL)

(define-sort |Z| () Int)
(declare-sort P 1)
(define-sort |POW Z| () (P |Z|))

(declare-const vmax |Z|)
(declare-const vset |POW Z|)
(declare-const |set.empty Z| |POW Z|)

(declare-fun |set.in Z| (|Z| |POW Z|) Bool)
(declare-fun max (|POW Z|) |Z|)

(assert (!
  (forall ((e |Z|))
    (not (|set.in Z| e |set.empty Z|)))
  :named |ax.set.in.empty Z|))

(assert (!
  (forall ((s |POW Z|))
    (=> (not (= s |set.empty Z|))
        (|set.in Z| (max s) s)))
  :named |ax.max.is.member|))

(assert (!
  (forall ((s |POW Z|) (e |Z|))
    (=> (|set.in Z| e s)
        (<= e (max s))))
  :named |ax.max.is.ge|))

(assert (!
  (not (= vmax (max vset)))
  :named |Goal|))

(check-sat)
(exit)

额外说明 #

• 修正符号引用后，CVC4 2.6可以正常解析并运行该代码，无需寻找2.7版本兼容的求解器。
• SMT-LIB中带竖线的标识符是整体符号，内部的竖线会被视为符号的一部分，而非分隔符，因此编写时需确保符号名完全一致。

内容的提问来源于stack exchange，提问作者Wissem Flitti