Z3の単純化戦術は正確に何をするのですか？

Question

Z3の戦術simplifyは正確に何をしているのですか？ Z3's official documentで は、それが言われている。

The command (simplify t) displays a possibly simpler expression equivalent to t. 

、このような戦術の機能は通常、誰も私がZ3のsimplifyは何書き換えをするのかを知らせることができ、Not(A or B) --> Not(A) and Not (B)のようないくつかの構文の書き換えルールを経由してまとめることができますので、？ありがとう。

Answer 1

書き換えルールについて説明するドキュメントはなく、コードやドキュメントにも構文ルールのリストはありません。正確に何が実行されているかを知るには、コードを見なければなりません。シンプル化の手法は、th_rewriter（here）を実行するだけで、数多くのクロス理論の簡略化（th_rewriter.cpp全体）が適用され、理論固有のリライタ（here）が呼び出されます。たとえば、ビットベクトルの用語については、bv_rewriter::reduce_app_coreを呼び出します。