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现在推荐的方法是让上下文首先创建一个求解器,然后直接在求解器上使用pushpop(在 Z3 4.0 之前没有求解器的概念)。Scala^Z3 还没有赶上,但您可以预期更改最终会传播。

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