z3 - 数値引数付きの * が単純化によって平坦化されないのはなぜですか?

Question

simplifyと:flat評価さ3 * x * y * zれると予想され(* 3 x y z)ます。代わりに、結果は(* 3 (* x y z))です。なんで？

例

w = Int('w')
x = Int('x')
y = Int('y')
z = Int('z')
print simplify(w * x * y * z, flat=True).num_args()  # 4, which we expected
print simplify(3 * x * y * z, flat=True).num_args()  # 2, why not 4?

Answer 1

Simplifier/Rewriter は、積をソルバーやその他の単純化/書き換え規則に便利な形式にします。この形式(* 3 (* x y z))は、合計を処理するときに便利です。たとえば、簡約器はルールをすばやく適用できます

(+ (* c t) (* d t)) --> (* (+ c d) t)

Z3 は最大限に共有された用語を使用するため、各製品のメモリには 1 つのコピーしかありません。この表現は、積を処理できる線形ソルバーにも役立ちます。(* x y z)彼らは農産物を新鮮な変数として扱うことができます。