【发布时间】：2019-01-06 00:21:51
【问题描述】：
在导入另一个文件中定义的函数和公理时，类似于 C 中的 #include。我无法在 SMTLIB 文档或在线示例中找到此类功能。有什么提示吗？
【问题讨论】：
【发布时间】：2019-01-06 00:21:51
【问题描述】：
SMTLib 无法#include'ing 或导入其他文件。这可能看起来像一个缺点，但人们手写 SMTLib 文件的情况很少见：它几乎总是由更高级别的语言机器生成的，并且假设生成 SMTLib 的人可以简单地吐出一个大文件包括您需要的一切。
话虽如此，我认为这个确实是一个有用的功能。 SMTLib 标准始终在不断发展，此类功能通常在其邮件列表中进行讨论：
https://groups.google.com/forum/#!forum/smt-lib
欢迎加入讨论并提出请求！
【讨论】：