smt2 中的类型不匹配答案

【问题标题】：Type mismatch in smt2smt2 中的类型不匹配
【发布时间】：2020-03-31 02:46:46
【问题描述】：

下面的 smt2 代码给出了与类型相关的错误。

( declare-datatypes ( ( List 1 ) )
  ( ( par ( T ) ( ( cons ( hd T ) ( tl ( List T ) ) )
 ( nil )
 ) )
 ) )

 (declare-sort Ty 0) 
(define-fun-rec func ((x (List Ty) ) (y (List Ty)))     (List Ty)
        (match  x   ( ((cons xt xts) ( cons xt (func xts y)) )
                      ( nil nil )
                    )
        )
)

错误：

(error "Both branches of the ITE must be a subtype of a common type.
then branch: ((lambda ((xt Ty) (xts (List Ty))) (cons xt (func xts y))) (hd x) (tl x))
its type   : (List Ty)
else branch: nil
its type   : (List T)
")

为什么它不使用返回类型，有什么办法吗？

一种方法是手动将其设置为 (nil (as nil (List Ty)) ) 以解决错误但我不想在程序中的每个 nil 处指定返回类型。还有其他方法吗？或者我需要提到的任何选项 enable ？

【问题讨论】：

标签： smt cvc4

【解决方案1】：

这是设计使然。 SMTLib 的类型系统并非旨在进行任何类型的推理，以使求解器轻松明确地加载规范。请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 3.6 节，其中讨论了良好排序要求。所以 CVC4 理所当然地拒绝了你的程序。

但你是对的，这在实践中相当烦人。典型的解决方案是一劳永逸地以您感兴趣的类型简单地定义所需的常量：

(define-fun nilTy () (List Ty) (as nil (List Ty)))

由于所有程序只能引用有限数量的排序，这总是可能的。（在实践中，无论如何，很少有超过几种不同类型的存在；所以它不是一个大负担。这有时被称为“单态化”。）

完成上述定义后，您只需在适当的上下文中使用它而不是 nil：

(define-fun-rec func ((x (List Ty) ) (y (List Ty)))     (List Ty)
        (match  x   ( ((cons xt xts) ( cons xt (func xts y)) )
                      ( nil nilTy)
                    )
        )
)

您会发现 CVC4 可以毫无困难地接受这一点，因为它现在确切地知道应该在哪个类别使用 nilTy。

请记住，SMTLib 通常不是手写的，而是机器生成的。因此，上述的笨拙通常并不适用，因为前端工具可以实现更高级的类型系统并在后台吐出所需的 SMTLib。希望对您有所帮助！

【讨论】：