3

我想使用 Scala^Z3 进行增量求解。在每次迭代中，我想

a）添加公式的一部分

b) 添加断言

应该为接下来的每次迭代保留公式，但如果我不能实现它，我需要删除断言，因为下一次迭代中的断言会有所不同。

那么有没有办法删除以前的语句？Z3Context.pop() 听起来有点像我需要的，但我找不到它的作用的描述..

将非常感谢那里的一些帮助！

最良好的祝愿，1428162

4

2 回答 2

3

是的，你是对的，你想pop（删除）最后一个断言。为此，您首先需要将当前的断言集保存为push. 这就是 Z3 支持作用域的方式。

通过添加公式的某些部分，我将假设您的意思是定义一个变量，其中包含您正在执行增量检查的一些原始大型公式的附加块。我还将假设原始公式是子公式的大合取。这个新公式将在推送和弹出之间保持定义（假设您保留一个引用它的变量）。

这是z3py中大致以下伪代码示例的链接，除了在z3py脚本中，我还假设公式和约束实际上是同一件事，但也许你想根据那块创建一些不同的约束子公式： http: //rise4fun.com/Z3Py/LIxW

我没有使用过 Scala^Z3，但大致上你想做以下事情：

formula // list containing parts (sub-formulas) of original large formula
while (formulaPart = formula.removeFirst()) // remove first element of list
    Z3Context.push() // save current set of assertions

    assertion = makeConstraint( formulaPart ) // assertion based on sub-formula

    Z3Context.assertCnstr( assertion ) // add new assertion

    if !Z3Context.check() // check if assertions cannot be satisfied
        Z3Context.pop() // remove most recent assertion

这是一个使用 .NET API 中的 pop/push 的示例：http ://research.microsoft.com/en-us/um/redmond/projects/z3/test__managed_8cs_source.html#l00637

您也会对此感兴趣：Z3 中的软/硬约束

于 2012-08-23T14:51:33.070 回答
2

没错，ctx.pop()就是你想要的。它也可以带一个参数，如ctx.pop(2)，但如果你省略它，它默认为 1。直观地说，将求解器的状态恢复到“n推送前”的位置。

所以如果你这样做：

ctx.assertCnstr(formula1)
ctx.push()

ctx.assertCnstr(extraAssertion)
ctx.check() match {
  case Some(true)  => ... // SAT
  case Some(false) => ... // UNSAT
  case None        => ... // UNKNOWN
}

ctx.pop(1)

...求解器的状态恢复到您调用之前的状态push()。

请注意，它们的行为与Z3 C API中的等效项完全相同，因此那里的文档也适用。

另请注意，从 Z3 4.0 开始，不推荐在上下文中调用push和。pop现在推荐的方法是让上下文首先创建一个求解器，然后直接在求解器上使用push和pop（在 Z3 4.0 之前没有求解器的概念）。Scala^Z3 还没有赶上，但您可以预期更改最终会传播。

于 2012-08-23T21:47:37.640 回答