smt2中的类型不匹配

Question

下面的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处指定返回类型。还有其他办法吗？还是我需要提及的任何选项启用？

Answer 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。希望能有所帮助！