z3 - Z3 の単純化

Question

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(simplify (or (= s ON) (= s OFF) (= s BROKEN)))
(simplify (and (> a 0) (> a 1)))

結果は次のとおりです。

(or (= s ON) (= s OFF) (= s BROKEN))
(and (not (<= a 0)) (not (<= a 1)))

しかし、予想された結果は次のとおりです。

1
> a 1

Z3 でそのような式 (そのような式の組み合わせ) を単純化することはできますか? ありがとうございました！

Answer 1

このsimplifyコマンドは、単なるボトムアップのリライターです。高速ですが、投稿のような表現を単純化することはできません。Z3を使用すると、ユーザーは戦術を使用して独自の単純化戦略を定義できます。これらについては、この記事とZ3チュートリアル（PythonおよびSMT 2.0）で説明しています。次の投稿にも追加情報があります。

• t>=1またはt>=2 => t> = 1
• ctx-solver-simplifyの非対称動作
• z3の「simplify」と「ctx-solver-simplify」の違いは何ですか

例の最初のクエリは、戦術を使用して簡略化できますctx-solver-simplify（オンラインでもここから入手できます）。

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(assert (or (= s ON) (= s OFF) (= s BROKEN)))
(assert (and (> a 0) (> a 1)))
(apply ctx-solver-simplify)

このコマンドは、一連のアサーションにapply戦術ctx-solver-simplifyを適用し、結果の一連の目標を表示します。この戦術はコマンドよりもはるかに高価であることに注意してくださいsimplify。