增量式SMT解算器具有降低特定约束的能力

Question

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

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

我想知道是否有任何增量解算器可以添加或删除由名称唯一标识的约束，或者是有其他方式处理它的API。我会很感激任何建议或意见。

Answer 1

基于“堆栈”的方法基本上是根深蒂固到SMTLib中的，所以我认为找到一个完全符合你想要的算法是很困难的。虽然我同意这将是一个很好的功能。

话虽如此，我可以想出两个解决方案。但是，两者都不能很好地服务于你的特定用例，尽管它们都将工作。事实上，您希望能够在每次致电check-sat时挑选自己的约束条件。不幸的是，这将是昂贵的。每当求解器做出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

使用复位断言和：全球声明

这是允许在每次调用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兼容的方式来做你想做的事情。然而，个人解决方案可能会有其他的技巧。您可能想要与他们的开发人员核对，看看他们是否可以为这个用例定制一些东西。虽然我怀疑是这样，但很高兴找到！

也看到尼古拉此以前的答案是非常相关的：How incremental solving works in Z3?