我还在学习Z3(Python)的内涵。
我注意到Z3 默认执行增量 SAT 求解(参见 Z3-Python中的 SAT 查询速度变慢：增量 SAT 呢？)：具体来说，每次使用s.add命令(其中s是求解器)时，这意味着它将该子句添加到s，但它不会忘记您以前学到的一切。
第一个问题：非增量SAT求解可以在Z3中完成吗？也就是说，以某种方式"停用"增量求解。这意味着什么？我们正在为每个放大的公式创建一个新的求解器？
例如，这种方法将是 Z3-default-incremental：
...
phi = a_formula
s = Solver()
s.add(phi)
while s.check() == sat:
s.check()
m = s.model()
phi = add_modelNegation(m)
s.add(phi) #in order not to explore the same model again
...
也就是说，一旦我们得到一个模型，我们就将被否定的模型附加到同一个求解器上。
虽然这个"强制"Z3是非增量的：
...
phi_st = a_formula
s = Solver()
s.add(phi_st)
negatedModelsStack = []
while s.check() == sat:
m = s.model()
phi_n = add_modelNegation(m)
negatedModelsStack.append(phi_n)
original_plus_negated = And(phi_st, And(negatedModelsStack))
s = Solver()
s.add(original_plus_negated) #in order not to explore the same model again
...
也就是说，一旦我们得到一个模型，我们就将获得的模型附加到一个新的求解器上。
我说的对吗？
另一方面，在附加的链接中，声明以下内容：
例如，将其与CVC4进行比较;默认情况下，CVC4不是增量的。如果要在增量模式下使用 CVC4，则必须传递特定的命令行参数
这是否意味着在CVC4中，您每次都必须创建一个新的求解器？就像在第二个代码中一样？
第二个问题：我怎样才能确切地知道我在Z3中使用什么技术进行增量求解？我一直在阅读有关增量SAT理论的文章，我看到其中一种技术是"CDCL"(http://www.cril.univ-artois.fr/~audemard/slidesMontpellier2014.pdf)，这是否用于Z3的增量搜索？
参考文献：为了不让类似的问题淹没 Stack，您建议对增量 SAT 和 Z3 的增量 SAT 使用哪些读数？另外，Z3 的增量 SAT 是否与其他求解器(如 MiniSAT 或 PySAT)的增量 SAT 相似？
我不确定你为什么要让 z3 以非增量方式行事。但是，如果这是你的目标，就不要多次打电话给check：这相当于非增量的。(将增量视为"附加功能"。您不必使用它。z3 和 cvc4 之间的唯一区别是后者需要您提前告诉它您打算以增量方式使用它，而前者默认是增量的。作为最终用户，您实际上不需要知道或关心差异。
旁注如果你启动 cvc4 而不告诉它是增量的，并调用check两次，它会抱怨。 z3 不会。但除此之外，体验应该是相同的。
从编程的角度来看，我不认为知道求解器如何增量实现真的很有帮助。(当然，如果您正在实现自己的 SMT 求解器，这一点至关重要。网上有很多关于SMT许多方面的论文，但如果你想从头开始研究这个话题，我推荐Daniel和Ofer关于决策程序的书：http://www.decision-procedures.org