首页 文章

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

提问于
浏览 次
4

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

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

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

z3 smt sat-solvers

1 回答

  • 4

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

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

    所以，我认为你留下了以下其中一个：

    使用check-sat-assume

    这基本上就是你所描述的 . 但回顾一下，你只需给它们起名字，而不是断言布尔 . 所以这：

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

    这确实增加了你必须管理的布尔常量的数量，但从某种意义上说，这些都是你想要的"names" . 我知道你不喜欢这个，因为它引入了很多变量;确实如此 . 这是有充分理由的 . 请在此处查看此讨论：https://github.com/Z3Prover/z3/issues/1048

    使用reset-assertions和：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

    等等，你是"remove"你不想要的 . 请注意 :global-declarations 调用非常重要，因为当您调用 reset-assertions 时，它将确保所有数据声明和其他绑定保持不变，这会告诉求解器从它假设和学习的内容开始 .

    实际上，您可以根据需要管理自己的约束 .

    摘要

    这些解决方案都不是您想要的，但它们都可以工作 . 如果不采用这两种解决方案之一，就没有符合SMTLib标准的方法来做你想做的事情 . 然而，个别解决者可能会有其他伎俩 . 您可能需要与他们的开发人员核实，看看他们是否可能为此用例提供自定义内容 . 虽然我怀疑是这种情况，但最好还是找出来！

    另请参阅Nikolaj之前的相关答案：How incremental solving works in Z3?

    回复于

相关问题