我可以在Z3中创建一个新的解算器吗？

我可以在Z3中创建一个新的求解器吗？在Z3中，创建解算器的标准过程如下所示：我可以在Z3中创建一个新的解算器吗？

context ctx; solver sv（ctx）;

经过插入断言和检查的过程之后，我想要创建一个新的求解器，比如说sv2，它相当于sv。但我找不到支持功能或API。解决费用昂贵，这是我不想从头开始创建sv2的方式。

陈婷

2015-10-05 Ting Chen

你是什么意思的“等值”？您可以根据需要创建尽可能多的解算器，但不会包含第一个解析器的断言。你当然可以将它们复制到新的求解器中，但我看不出如何使任何更便宜的东西。 –

是的，就像你说的那样，将旧解算器中的所有断言复制到新解释器并不会使任何便宜。我相信通过这种方式，我必须解决我在旧解算器中已经解决的问题。那么有没有便宜的方法。我的意思是从一个旧的求解器中创建一个新求解器，同时保持其状态，从而逐步解决问题。 –

这样做，可以通过多种方法推/拉或下假设（都在同一求解器和上下文）来解决，看Soft/Hard constraints in Z3，Z3/SMT: When should I prefer push/pop to reset?的常用方式。另外，搜索这些关键词，关于这个问题还有很多问题和答案。

2015-10-05 12:47:49

回答