Module Tolk.Symbolic

uop_given_valid valid u is u simplified with Shape.symbolic, knowing that the boolean valid holds. Each clause of the conjunction valid that bounds an integer expression, e < c, c < e or not (e < c), is assumed by replacing e with a variable of those bounds. With try_simplex (default true), a clause stating that a sum of irreducible terms is at least 1 also tries each term at least 1 in turn, and keeps the result they all agree on. A loop's range stays as it is, its bound included: assumed inside the bound, a clause would make another loop. The result has u's values wherever valid holds.

simplify_valid valid is the conjunction valid with each clause simplified knowing that the clauses before it hold (uop_given_valid), after removing duplicates and ordering the clauses so that one whose expression others depend on, then one of tighter bounds, comes first. It is None if nothing changes or valid involves an Op.t.Index.

pm_simplify_valid simplifies each boolean conjunction with simplify_valid, and the weak integer value of each gate knowing its condition holds (uop_given_valid, without try_simplex) when it involves no Op.t.Index.

pm_drop_and_clauses drops from each gate's condition the clauses that run in none of the gated value's ranges.

pm_move_where_on_load turns a selection between a load's index and 0 into a load gated by the selection's condition: each clause that the index does not already require, that is not constant, that runs in no range the index lacks and that reads no other Op.t.Index moves into the index's gate; the others stay in the selection. A gated load reads +0. where its gate fails, so a selection of -0. is left as it is.

pm_clean_up_group_sink splices into each sink the sources of its Op.t.Noop, Op.t.Stack, Op.t.Sink and Op.t.After sources.

sym is Shape.symbolic and pm_simplify_valid, followed by:

• powers: a float Op.t.Pow is computed from exp2 and log2 (Transcendental.xpow), and an integer one by repeated squaring (Transcendental.xpow_int);
• stores: storing to an index what a load from that index reads does nothing; storing where g alt (load index) stores alt where g holds, and where g (load index) alt where it does not; storing Ops.invalid does nothing, and storing a gated value stores it where its gate holds;
• reductions: the factors of an integer reduced product that do not depend on the reduction's ranges move out of a sum, and out of a maximum when they are non-negative;
• terms: (x + y) * c is x * c + y * c for weak integers, where each value multiplied Shape.fits;

then cleans up groups and sinks (pm_clean_up_group_sink).