C比z3的标准输入z3更有问题吗？

Question

我对z3完全陌生。我想知道这两个输入之间有什么区别，C比z3的标准输入z3更有问题吗？如果您可以answer_(：з“∠)_)，我将不胜感激。

Answer 1

我不知道你所说的“有问题”是什么意思。“如果要将z3集成到基于C/C++的框架中，可以使用C。如果您想要一种被许多求解者理解的通用语言，而不仅仅是SMTLib，您可以使用z3。所以，这取决于你的目标是什么。

如果您只是在试验它，我建议您使用更高级的语言(如Python )的接口，因为它要容易得多。SMTLib一般不是供人类使用的，而是由其他程序生成的。只有当您有其他需要保持在C/C++中的需求时，才使用C/C++ API。

长话短说，这真的取决于你的目标是什么；如果你告诉我们更多你的用例是什么，我们可以推荐一些更具体的东西。