-- If the ``monotonicAggregates`` language pragma is not enabled, or the original formula and variable declarations are both omitted, then the aggregate is transformed as follows: - For each aggregation expression ``expr_i``, a fresh variable ``v_i`` is declared with the same type as the expression in addition to the original variable declarations. - The new range is the conjunction of the original range and a term ``v_i = expr_i`` for each aggregation expression ``expr_i``. - Each original aggregation expression ``expr_i`` is replaced by a new aggregation expression ``v_i``.
0 commit comments