2

https://git01.codeplex.com/z3 (89c1785b)ctx-solver-simplifyのマスター ブランチから Z3 の最新バージョンを使用して、z3.And() へのパラメーターの順序が重要であるように思われるから、かなり驚くべき動作が見られます。

#!/usr/bin/python
import z3

a, b = z3.Bools('a b')
p = z3.Not(a)
q = z3.Or(a, b)
for e in z3.And(p, q), z3.And(q, p):
  print e, '->', z3.Tactic('ctx-solver-simplify')(e)

生成:

And(Not(a), Or(a, b)) -> [[Not(a), Or(a, b)]]
And(Or(a, b), Not(a)) -> [[b, Not(a)]]

これはZ3のバグですか？

4

2 に答える 2

2

基本的にカノニシティを要求する場合、他のトレードオフがあるため、カスタム タクティクスを作成する方がよいと思います。Z3 には、数式を正規の形式に変換する戦術はありません。したがって、地面と等価な式に対して常に同じ答えを生成するものが必要な場合は、これを保証する新しいノーマライザーを作成する必要があります。

ctx_solver_simplify_tactic はさらに、式を単純化するときにいくつかのトレードオフを行います。同じサブ式を複数回単純化することを回避します。もしそうなら、結果の式のサイズが大幅に（指数関数的に）増加する可能性があります。

于 2012-11-29T16:18:24.983 に答える
2

いいえ、これはバグではありません。この戦術ctx-solver-simplifyは非常に高価で、本質的に非対称です。つまり、サブ式が参照される順序が最終結果に影響します。この戦術はファイルに実装されていますsrc/smt/tactic/ctx_solver_simplify_tactic.cpp。コードはかなり読みやすいです。「SMT」ソルバー ( ) を使用し、入力式をトラバースm_solverしながら を複数回呼び出すことに注意してください。m_solver.check()これらの呼び出しのそれぞれは、非常に高価になる可能性があります。特定の問題領域については、この戦術のさらに高価なバージョンを実装し、質問で説明されている非対称性を回避できます。

編集：

戦術 も検討できます。ctx-simplifyこれは より安価ですがctx-solver-simplify、対称的です。この戦術ctx-simplifyは、基本的に次のようなルールを適用します。

A \/ F[A] ==> A \/ F[false]
x != c \/ F[x] ==> F[c]

F[A]を含む可能性のある数式はどこにありますかA。ctx-solver-simplify数式をトラバースするときに SMT ソルバーを呼び出さないため、より安価です。この戦術を使用した例を次に示します (オンラインでも入手可能):

a, b = Bools('a b')
p = Not(a)
q = Or(a, b)
c = Bool('c')
t = Then('simplify', 'propagate-values', 'ctx-simplify')
for e in Or(c, And(p, q)), Or(c, And(q, p)):
  print e, '->', t(e)

人間の可読性に関しては、これは戦術を実装する際の目標ではありませんでした。上記の戦術があなたの目的に十分でない場合はお知らせください。

于 2012-11-29T07:54:51.197 に答える