【发布时间】：2022-01-27 07:07:32
【问题描述】：
我对 z3 完全陌生。我想知道这两个输入之间有什么区别，C API 是否比 z3 的标准输入 SMTLIB2 更成问题？如果你能回答我将不胜感激_(:з」∠)_
【问题讨论】：
-
请澄清您的具体问题或提供其他详细信息以准确突出您的需求。正如目前所写的那样，很难准确地说出你在问什么。
【发布时间】：2022-01-27 07:07:32
【问题描述】：
我不确定您所说的“有问题”是什么意思。如果您想将 z3 集成到基于 C/C++ 的框架中，您将使用 C-API。如果您想要一种被许多求解器（而不仅仅是 z3）理解的通用语言，您将使用 SMTLib。所以，这真的取决于你的目标是什么。
如果您只是在尝试它，我建议您使用 Python 等高级语言的接口，因为它更容易上手。 SMTLib 通常不是供人类使用的，而是由其他程序生成的。仅当您有其他需要使用 C/C++ 的要求时才使用 C/C++ API。
长话短说，这真的取决于你的目标是什么；如果您告诉我们更多关于您的用例的信息，我们可以推荐更具体的内容。
【讨论】：
-
我需要制作一个用于验证程序的工具，比如不锈钢。使用c API开发更方便，但我担心API会带来一些我用smtlib不会遇到的问题。不知道有没有说清楚，非常感谢
-
C API 坚如磐石。实际上，大多数其他语言的 API 都是建立在 C-API 之上的。当然，与其他绑定相比，它更难使用，但它可以直接访问 z3 的每个部分。如果您的验证环境的其余部分将用 C 编写，那么请务必使用 z3 的 C API。