smt2 中的类型不匹配
Type mismatch in smt2
下面的 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)
")
为什么它无法使用 return 类型,有什么方法可以做到这一点吗?
一种方法是手动将其设置为 (nil (as nil (List Ty)) )
以解决错误但我不想在程序中的每个 nil 处指定 return 类型。
还有其他办法吗?或我需要提及的任何选项启用?
这是设计使然。 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)))
由于所有程序只能引用有限数量的排序,所以这总是可能的。 (在实践中,无论如何,很少有超过几种不同的类型存在;所以这不是一个很大的负担。这有时被称为 "monomorphisation.")
一旦你做了上面的定义,那么你只需在适当的上下文中使用它而不是 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。希望对您有所帮助!
下面的 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)
")
为什么它无法使用 return 类型,有什么方法可以做到这一点吗?
一种方法是手动将其设置为 (nil (as nil (List Ty)) )
以解决错误但我不想在程序中的每个 nil 处指定 return 类型。
还有其他办法吗?或我需要提及的任何选项启用?
这是设计使然。 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)))
由于所有程序只能引用有限数量的排序,所以这总是可能的。 (在实践中,无论如何,很少有超过几种不同的类型存在;所以这不是一个很大的负担。这有时被称为 "monomorphisation.")
一旦你做了上面的定义,那么你只需在适当的上下文中使用它而不是 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。希望对您有所帮助!