srg*_*srg 5 sat-solvers smt z3
是否有增量 SMT 求解器或某些增量 SMT 求解器的 API，我可以在其中增量添加约束，在其中我可以通过某些标签/名称唯一标识每个约束？
我想唯一地标识约束的原因是，我可以稍后通过指定该标签/名称来删除它们。需要删除约束是因为我之前的约束随着时间变得无关紧要。我看到使用 Z3 我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。使用基于假设的 Z3 的其他增量方法，我将不得不执行格式“(check-sat p1 p2 p3)”的 check-sat，即如果我有三个断言要检查，那么我将需要三个布尔常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个布尔常量。我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，
我想知道是否有任何增量求解器可以添加或删除由名称唯一标识的约束，或者有其他方法来处理它的 API。我将不胜感激任何建议或意见。
基于“堆栈”的方法在 SMTLib 中根深蒂固，所以我认为很难找到一个完全符合您要求的求解器。虽然我同意这将是一个不错的功能。
话虽如此，我可以想到两种解决方案。但是它们都不能很好地服务于您的特定用例，尽管它们都可以工作。归结为您希望能够在每次调用check-sat. 不幸的是，这将是昂贵的。每次求解器执行 a 时，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
这是允许您在每次调用时任意挑选断言的变体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 中进行增量求解？