BackoffRuleApplication
A saturation strategy that applies rules with a backoff heuristic.
Rules are initially allowed to apply a limited number of matches. Once this quota is exhausted, the rule is banned for a fixed number of iterations. After the ban period ends, the rule is re-enabled with both its match limit and ban duration doubled. This encourages frequent early exploration and gradual fading out of overly eager rules.
Rules apply up to their remaining match limits each iteration, chosen uniformly at random from the match set.
Type parameters
- EGraphT
-
The type of the e-graph.
- MatchT
-
The type of rule match.
- NodeT
-
The node type in the e-graph.
- RuleT
-
The rewrite rule type.
Value parameters
- rules
-
Rules annotated with initial match limits and ban lengths.
- searchAndApply
-
Strategy for finding and applying rule matches to the e-graph.
Attributes
- Graph
-
- Supertypes
-
trait Serializabletrait Producttrait Equalsclass Objecttrait Matchableclass AnyShow all
Members list
Value members
Concrete methods
Applies a single iteration of the strategy.
Applies a single iteration of the strategy.
Value parameters
- data
-
Data that is carried forward from one iteration to the next.
- egraph
-
The e-graph to saturate.
- parallelize
-
The parallelization strategy to use.
Attributes
- Returns
-
The new e-graph and data. The new e-graph is
Noneif the strategy did not make any changes to the e-graph. - Definition Classes
The initial data for the strategy's first iteration.
Inherited methods
Applies the strategy to an e-graph with the initial data.
Applies the strategy to an e-graph with the initial data.
Value parameters
- egraph
-
The e-graph to saturate.
- parallelize
-
The parallelization strategy to use.
Attributes
- Returns
-
The new e-graph. The new e-graph is
Noneif the strategy did not make any changes to the e-graph. - Inherited from:
- Strategy
Creates a strategy that drops the data carried by this strategy, running each iteration with the initial data.
Creates a strategy that drops the data carried by this strategy, running each iteration with the initial data.
Attributes
- Returns
-
A new strategy that applies this strategy without carrying any data.
- Inherited from:
- Strategy
Attributes
- Inherited from:
- Product
Attributes
- Inherited from:
- Product
Creates a strategy that repeatedly applies iterations of this strategy until a fixpoint is reached. The data carried by the strategy is initialized at the start of the repetition, carried forward through each iteration, and dropped at the end of the repetition.
Creates a strategy that repeatedly applies iterations of this strategy until a fixpoint is reached. The data carried by the strategy is initialized at the start of the repetition, carried forward through each iteration, and dropped at the end of the repetition.
Attributes
- Returns
-
A new strategy that applies this strategy until a fixpoint is reached.
- Inherited from:
- Strategy
Creates a strategy that repeatedly applies iterations of this strategy until a fixpoint is reached. State is carried forward from one iteration to the next, allowing the strategy to accumulate changes from one repetition to the next.
Creates a strategy that repeatedly applies iterations of this strategy until a fixpoint is reached. State is carried forward from one iteration to the next, allowing the strategy to accumulate changes from one repetition to the next.
Attributes
- Returns
-
A new strategy that applies this strategy until a fixpoint is reached.
- Inherited from:
- Strategy
Chains another strategy to this strategy. The resulting strategy applies this strategy first, and then applies the other strategy to the result of this strategy.
Chains another strategy to this strategy. The resulting strategy applies this strategy first, and then applies the other strategy to the result of this strategy.
Type parameters
- Data2
-
The type of the data carried by the other strategy.
Value parameters
- other
-
The other strategy to chain with this strategy.
Attributes
- Returns
-
A new strategy that applies this strategy followed by the other strategy.
- Inherited from:
- Strategy
Wraps this strategy with a logger that observes and logs changes to the e-graph after each iteration.
Wraps this strategy with a logger that observes and logs changes to the e-graph after each iteration.
This is useful for debugging or analysis purposes, as it provides visibility into the differences between successive versions of the e-graph produced by the strategy. If the strategy does not modify the e-graph during an iteration, the logger is not invoked.
Value parameters
- logChange
-
A function that takes the previous and updated e-graphs and performs logging or inspection.
Attributes
- Returns
-
A new strategy that behaves identically to this one, but logs changes whenever they occur.
- Inherited from:
- Strategy
Creates a strategy that runs this strategy with an optional limit on the number of iterations.
Creates a strategy that runs this strategy with an optional limit on the number of iterations.
Value parameters
- limit
-
An optional limit on the number of iterations. If the limit is defined, the strategy will run with the specified limit. If the limit is not defined, the strategy will run without a limit.
Attributes
- Returns
-
A new strategy that applies this strategy with an optional limit on the number of iterations.
- Inherited from:
- Strategy
Creates a strategy that places a limit on the number of iterations. The limit is the maximum number of iterations that the strategy will run. Once the limit is reached, additional applications of the strategy will make no further changes to the e-graph.
Creates a strategy that places a limit on the number of iterations. The limit is the maximum number of iterations that the strategy will run. Once the limit is reached, additional applications of the strategy will make no further changes to the e-graph.
Value parameters
- limit
-
The maximum number of iterations to run the strategy. If the limit is zero, the strategy will never change the e-graph.
Attributes
- Returns
-
A new strategy that applies this strategy with a limit on the number of iterations.
- Inherited from:
- Strategy
Lifts this strategy to operate on an e-graph with a root. The root is typically used to extract trees from the e-graph.
Lifts this strategy to operate on an e-graph with a root. The root is typically used to extract trees from the e-graph.
Attributes
- Returns
-
A new strategy that operates on an EGraphWithRoot.
- Inherited from:
- Strategy
Creates a strategy that runs this strategy with an optional timeout.
Creates a strategy that runs this strategy with an optional timeout.
Value parameters
- timeout
-
An optional timeout for the strategy. If the timeout is defined, the strategy will run with the specified timeout. If the timeout is not defined, the strategy will run without a timeout.
Attributes
- Returns
-
A new strategy that applies this strategy with an optional timeout.
- Inherited from:
- Strategy
Creates a strategy that runs this strategy with a timeout.
Creates a strategy that runs this strategy with a timeout.
Value parameters
- timeout
-
The timeout for the strategy. If the strategy does not complete within the timeout, it is canceled. The timeout is a time budget that is shared across all iterations of the strategy.
Attributes
- Returns
-
A new strategy that applies this strategy with a timeout.
- Inherited from:
- Strategy