5

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

我想唯一标识约束的原因是我以后可以通过指定该标签/名称来删除它们。需要放弃约束是因为我之前的约束与时间无关。我看到在 Z3 中我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。使用基于假设的 Z3 的其他增量方法，我将不得不执行格式为“(check-sat p1 p2 p3)”的 check-sat，即如果我要检查三个断言，那么我将需要三个布尔常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个布尔常量。我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，

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

4

1 回答 1

6

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

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

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

使用检查坐假设

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

  (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..))

这确实增加了您必须管理的布尔常量的数量，但从某种意义上说，这些都是您想要的“名称”。我知道您不喜欢这样，因为它引入了很多变量；确实如此。这是有充分理由的。在此处查看此讨论：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调用很重要，因为它将确保您的所有数据声明和其他绑定在您调用时保持不变reset-assertions，这告诉求解器从它假设和学习的内容开始。

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

概括

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

另请参阅 Nikolaj 的先前答案，该答案非常相关：Z3 中增量求解的工作原理？

于 2017-06-04T18:23:48.747 回答