AngouriMath
EqualitySaturation(AngouriMath.Core.Budgets.WorkBudget,AngouriMath.Core.CostModel)
Method (no overloads)
Summary
Explores the equalities the whole registry's rules reach from an expression at once,
over an e-graph, and extracts the cheapest undercostModel .
over an e-graph, and extracts the cheapest under
Parameter "budget"
What this call may spend before it settles for the best it has found so far.
Steps is charged once per e-node the graph actually creates;
Time is the wall-clock backstop. A caller who sets
Budget overrides this, the same as every other bounded
computation in the library.
Steps is charged once per e-node the graph actually creates;
Time is the wall-clock backstop. A caller who sets
Budget overrides this, the same as every other bounded
computation in the library.
Parameter "costModel"
Which candidate counts as cheapest once exploration stops.
Remarks
RationalCanonicalization and Canonicalization, and for a
sharper reason:
so an expanding rule and a collecting one never meet — the order they run in decides
which wins. Equality saturation deletes that order and keeps every result, which is
why it needs a budget rather than a pass count, and why only the rules a scheduler can
prove will not run away are offered to it — see the next paragraph.
Collects or Rearranges,
and whose Soundness is at least
SoundUnderAssumptions, are used — the population is
All, not the public registry. Growth is derived
from the pattern tree for a rule whose replacement is itself a pattern, and declared
explicitly by the rule's own author for a rule whose replacement is code, which is what
let a further batch of code-built rules earn a place here without being able to lie
about it. Unknown is withheld either way: a rule nobody
has justified is not proven safe, and not proven safe is not the same as safe. This is
#746 tier 2's
e-graph. As of this writing the filter passes 43 rules.
back to materialising a term where it cannot. A rule's
CanEMatch on its Left decides per rule: where it is true this asks the e-graph directly, which is what a
production e-matcher over MatchPattern is supposed to do; where
it is false this falls back to extracting a term and rewriting that instead — slower,
and the only path the harness this is built from ever took. Of the 43 rules the filter
above passes, roughly 27-28 can actually build a replacement today; the remaining ~15
each build a boolean connective or a turned-around equality (
but cannot fire, because EGraph's reconstruction whitelist has no entry
for any of those node types yet and
class that needs one. That is a separate, already-known limitation of
EGraph itself — see
cover those six node types, all 15 go live at once, which is the moment to re-run
measurement — a textbook corpus of 16 expressions, all of which saturated — was made
under a much larger rule set (313 rules, off the public registry's string-length
RewriteRuleGrowth proxy), before the Soundness filter existed
and before any rule here could e-match at all, so it does not describe this population —
a different source, a different filter, a different matcher — and should not be cited as
though it still does without being re-run. Even re-run, a corpus
saturating says the graph stopped growing on those inputs; it did not and could not say
that of every expression
that this is still being found out, not one sized for how much the caller can afford to
lose.
Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online