z3 - 具有删除特定约束能力的增量 SMT 求解器

Question

是否有增量 SMT 求解器或某些增量 SMT 求解器的 API，我可以在其中增量添加约束，我可以通过某个标签/名称唯一标识每个约束？

我想唯一标识约束的原因是我以后可以通过指定该标签/名称来删除它们。
需要放弃约束是因为我之前的约束与时间无关。
我看到在 Z3 中我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。
使用基于假设的 Z3 的另一种增量方法，我将不得不执行格式为“(check-sat p1 p2 p3)”的 check-sat，即如果我要检查三个断言，那么我将需要三个 bool 常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个 bool 常量。
我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，以查看该 API 是否提供了一些更好的方法来处理此要求，但我只看到通过“addConstraint”或“push”添加约束的方法，并且无法找到任何方法删除或删除特定约束，因为 pop 是唯一可用的选项。

我想知道是否有任何增量求解器可以添加或删除由名称唯一标识的约束，或者是否有 API 可以使用另一种方法来处理它。我将不胜感激任何建议或意见。

Answer 1

基于“堆栈”的方法在 SMTLib 中根深蒂固，因此我认为很难找到一个完全符合您要求的求解器。虽然我同意这将是一个不错的功能。

话虽如此，我可以想到两种解决方案。但是两者都不能很好地服务于您的特定用例，尽管它们都可以工作。归根结底，您希望能够在每次调用 check-sat 时挑选您的约束。 .不幸的是，这将是昂贵的。每次求解器执行 check-sat它基于所有现有的断言学习了很多引理，并且相应地修改了很多内部数据结构。基于堆栈的方法本质上允许求解器“回溯”到这些学习状态之一。但是，当然，这不允许像您观察到的那样 cherry-pick 。

所以，我认为你只剩下以下之一:

使用检查坐假设

这基本上就是你已经描述的。但回顾一下，您只需给它们命名，而不是断言 bool 值。所以这:

  (assert complicated_expression)

变成

  ; for each constraint ci, do this:
  (declare-const ci Bool)
  (assert (= ci complicated_expression))
  ; then, check with whatever subset you want
  (check-sat-assuming (ci cj ck..))

这确实增加了您必须管理的 bool 常量的数量，但从某种意义上说，这些都是您想要的“名称”。我知道您不喜欢这样，因为它引入了很多变量；确实如此。这是有充分理由的。在此处查看此讨论: https://github.com/Z3Prover/z3/issues/1048

使用重置断言和 :global-declarations

这是允许您在每次调用 check-sat 时任意挑选断言的变体。 .但它不会便宜。特别是，每次你按照这个秘诀学习时，求解器都会忘记它所学到的一切。但它会做你想要的。首要问题:

(set-option :global-declarations true)

并以某种方式自己在包装中跟踪所有这些。现在，如果你想任意“添加”一个约束，你不需要做任何事情。只需添加它。如果你想删除一些东西，那么你说:

 (reset-assertions)
 (assert your-tracked-assertion-1)
 (assert your-tracked-assertion-2)
;(assert your-tracked-assertion-3)  <-- Note the comment, we're skipping
 (assert your-tracked-assertion-4) 
 ..etc

等等。也就是说，你“删除”你不想要的那些。请注意 :global-declarations call 很重要，因为它会确保您在调用 reset-assertions 时所有数据声明和其他绑定(bind)都保持不变。 ，它告诉求解器从它假设和学习的内容开始。

实际上，您正在管理自己的约束，正如您最初想要的那样。

概括

这些解决方案都不是您想要的，但它们会起作用。如果不求助于这两种解决方案之一，根本就没有符合 SMTLib 的方法来做你想做的事。然而，个别求解者可能还有其他技巧。您可能想与他们的开发人员核实，看看他们是否有针对此用例的自定义内容。虽然我怀疑是这种情况，但很高兴发现!

另请参阅 Nikolaj 的先前答案，该答案非常相关: How incremental solving works in Z3?