z3 - 为什么带数字参数的 * 没有被简化展平？

Question

我希望simplifywith:flat评估3 * x * y * zto (* 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

简化器/重写器将产品以便于求解器和其他简化/重写规则的格式放置。该格式(* 3 (* x y z))在处理总和时很方便。例如，简化器可以快速应用规则

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

Z3 使用最大共享术语，那么每个产品的内存中只有一个副本。该表示对于可以处理产品的线性求解器也很有用。他们可以将农产品(* x y z)视为新鲜的变量。