具有删除特定约束能力的增量 SMT 求解器 [英] Incremental SMT solver with ability to drop specific constraint

问题描述

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

Is there an incremental SMT solver or an API for some incremental SMT solver where I can add constraints incrementally, where I can uniquely identify each constraint by some label/name?

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

The reason I want to identify the constraints uniquely is so that I can drop them later by specifying that label/name. The need for dropping constraints is due to the fact that my earlier constraints become irrelevant with time. I see that with Z3 I cannot use the push/pop based incremental approach because it follows a stack based idea whereas my requirement is to drop specific earlier/old constraints. With the other incremental approach of Z3 based on assumptions, I would have to perform check-sat of the format "(check-sat p1 p2 p3)" i.e. if I had three assertions to check then I would require three boolean constants p1,p2,p3, but in my implementation I would have thousands of assertions to check at a time, indirectly requiring thousands of boolean constants. I also checked JavaSMT, a Java API for SMT solvers, to see if the API provides some better way of handling this requirement, but I see only way to add constraints by "addConstraint" or "push" and was unable to find any way of dropping or removing specific constraints since the pop is the only option available.

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

I would like to know if there is any incremental solver where I can add or drop constraints uniquely identified by names, or an API where there is an alternative way to handle it. I would appreciate any suggestion or comments.

推荐答案

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

The "stack" based approach is pretty much ingrained into SMTLib, so I think it'll be tough to find a solver that does exactly what you want. Although I do agree it would be a nice feature.

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

Having said that, I can think of two solutions. But neither will serve your particular use-case well, though they will both work. It comes down to the fact that you want to be able to cherry-pick your constraints at each call to check-sat. Unfortunately this is going to be expensive. Each time the solver does a check-sat it learns a lot of lemmas based on all the present assertions, and a lot of internal data-structures are correspondingly modified. The stack-based approach essentially allows the solver to "backtrack" to one of those learned states. But of course, that does not allow cherry-picking as you observed.

所以，我认为您会遇到以下情况之一:

So, I think you're left with one of the following:

这基本上就是您已经描述的内容.但是回顾一下，您只需为它们命名，而不是断言布尔值.所以，这:

This is essentially what you described already. But to recap, instead of asserting booleans, you simply give them names. So, this:

  (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

This does increase the number of boolean constants you have to manage, but in a sense these are the "names" you want anyhow. I understand you do not like this as it introduces a lot of variables; and that is indeed the case. And there's a good reason for that. See this discussion here: https://github.com/Z3Prover/z3/issues/1048

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

This is the variant that allows you to arbitrarily cherry-pick the assertions at each call to check-sat. But it will not be cheap. In particular, the solver will forget everything it learned each time you follow this recipe. But it will do precisely what you wanted. First issue:

(set-option :global-declarations true)

并以某种方式在您的包装器中跟踪所有这些.现在，如果你想随意添加"一个约束，你不需要做任何事情.只需添加它.如果您想删除某些内容，请说:

And somehow keep track of all these yourself in your wrapper. Now, if you want to arbitrarily "add" a constraint, you don't need to do anything. Just add it. If you want to remove something, then you say:

 (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 时，它会确保所有数据声明和其他绑定保持完整，它告诉求解器从它假设和学到的东西开始.

etc. That is, you "remove" the ones you don't want. Note that the :global-declarations call is important since it'll make sure all your data-declarations and other bindings stay intact when you call reset-assertions, which tells the solver to start from a clean-slate of what it assumed and learned.

实际上，您可以按照自己的意愿管理自己的约束条件.

Effectively, you're managing your own constraints, as you wanted in the first place.

这些解决方案都不是您想要的，但它们会起作用.如果不求助于这两种解决方案中的一种，根本就没有符合 SMTLib 的方法来做您想做的事情.然而，个别求解器可能有其他技巧.您可能想咨询他们的开发人员，看看他们是否有针对此用例的自定义内容.虽然我对此表示怀疑，但如果能找到答案会很高兴！

Neither of these solutions is precisely what you wanted, but they will work. There's simply no SMTLib compliant way to do what you want without resorting to one of these two solutions. Individual solvers, however, might have other tricks up their sleeve. You might want to check with their developers to see if they might have something custom for this use case. While I doubt that is the case, it would be nice to find out!

另请参阅 Nikolaj 之前的回答，这是非常相关的:How增量求解在 Z3 中有效吗?

Also see this previous answer from Nikolaj which is quite related: How incremental solving works in Z3?

这篇关于具有删除特定约束能力的增量 SMT 求解器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！