3

増分解決にScala^Z3を使用したいと思います。各反復で私はしたい

a）数式の一部を追加します

b）アサーションを追加する

数式は後続の反復ごとに保持する必要がありますが、次の反復でのアサーションが異なるため、それを実行できない場合は、アサーションを削除する必要があります。

では、前のステートメントを削除する方法はありますか？Z3Context.pop（）は私が必要としているものに少し似ていますが、それが何をするのかについての説明が見つかりませんでした。

そこで助けてくれてとてもありがたいです！

よろしくお願いします、1428162

4

2 に答える 2

3

Yes, you're right, you want to pop (remove) the last assertion. To do this, you first need to save the current set of assertions with push. This is how Z3 supports scope.

By add some part of the formula, I'm going to assume you mean to define a variable containing an additional chunk of some original large formula you're doing the incremental checking on. I'll also assume the original formula is a large conjunction of sub-formulas. This new formula will remain defined between pushes and pops (assuming you keep a variable referencing it).

Here is a link to an example of roughly the following pseudo-code in z3py, except in the z3py script I also assume the formula and the constraint are actually the same thing, but maybe you want to create some different constraint based on that piece of the subformula: http://rise4fun.com/Z3Py/LIxW

I haven't used Scala^Z3, but roughly you want to do the following:

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

Here is an example using pop/push from the .NET API: http://research.microsoft.com/en-us/um/redmond/projects/z3/test__managed_8cs_source.html#l00637

You'd also be interested in this: Soft/Hard constraints in 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()。

これらはZ3CAPIとまったく同じように動作するため、そこからのドキュメントも適用されることに注意してください。

pushZ3 4.0では、コンテキストでの呼び出しpopは非推奨になっていることにも注意してください。推奨される方法は、コンテキストで最初にソルバーを作成し、次にソルバーを直接使用するpushことpopです（Z3 4.0より前のソルバーの概念はありませんでした）。Scala ^ Z3はまだ追いついていないが、変更が最終的には伝播されることが期待できる。

于 2012-08-23T21:47:37.640 に答える