【发布时间】：2023-04-05 09:04:02
【问题描述】：
在我的研究中，我自动生成 SMT2，然后将其传递给 Z3。生成的代码基本上是许多不同约束的一个非常大的连词(and ...)。
这样做会不会失去（或获得？）任何显着的性能，而不是生成许多断言？
【问题讨论】：
-
我敢说你不会得到你的问题的明确答案，因为你没有提供任何关于你的约束所涉及的理论的细节。即使你这样做了，可能仍然很难让人满意。我建议您先进行实验（生成两个形状），如果需要，请返回此处报告您的发现并根据这些发现改进您的问题。