Z3中的解释函数和未解释函数有什么区别？

问题描述

在阅读针对Z3的快速LCF样式证明重构时，我了解到Z3的语言中存在诸如+或forall的解释函数。我猜也有未解释的功能。两者有什么区别？

解决方法

它们是具有名称和签名但没有定义的函数，请参见Uninterpreted Function。