CODEWITHSUNDEEP
z3z3py
thpani
thpani

Reputation: 423

Why is * with numeral argument not flattened by simplify?

I would expect simplify with :flat to evaluate 3 * x * y * z to (* 3 x y z). Instead, the result is (* 3 (* x y z)). Why?

Example

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?

Upvotes: 0

Views: 68

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The simplifier/rewriter puts products in a format that is convenient for solvers and other simplification/rewrite rules. The format (* 3 (* x y z)) is convenient when processing sums. For example, the simplifier can quickly apply the rule 

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

Z3 uses maximally shared terms, then there is only one copy in memory of each product. The representation is also useful for linear solvers that can handle products. They can treat the produce (* x y z) as a fresh variable.

Upvotes: 2

Related Questions