TransformAndRebase

foresight.eqsat.saturation.TransformAndRebase
See theTransformAndRebase companion object
final case class TransformAndRebase[NodeT, EGraphT <: EGraphLike[NodeT, EGraphT] & EGraph[NodeT], Data](transform: Strategy[NodeT, EGraphT, Data], extractor: Extractor[NodeT, EGraphT], getRoot: EGraphT => EClassCall, setRoot: (EGraphT, EClassCall) => EGraphT, areEquivalent: (Tree[NodeT], Tree[NodeT]) => Boolean) extends Strategy[NodeT, EGraphT, (Data, Option[Tree[NodeT]])]

A compound strategy that transforms an e-graph and optionally rebases it by extracting and reinserting a tree.

This strategy wraps a transformation strategy (transform) and augments it with tree rebasing semantics:

  1. The inner strategy is first applied to the e-graph.
  2. If it produces no change, the strategy halts and rebasing is skipped.
  3. If it does change the e-graph, the new tree rooted at a given foresight.eqsat.EClassCall is extracted.
  4. If the newly extracted tree is equivalent (according to areEquivalent) to the previous one, rebasing is skipped.
  5. Otherwise, the new tree is added to an empty e-graph, producing a new root and a freshly rooted e-graph.

This approach is especially useful in fixpoint-style optimization loops, where you want to:

  • Track convergence at the level of extracted trees, not just internal graph structure.
  • Avoid redundant re-extractions and expansions.
  • Restart from a canonical or minimal representative tree when changes occur.

Type parameters

Data

The internal state type carried by the transformation strategy.

EGraphT

The type of the e-graph, usually a wrapper like EGraphWithRoot or foresight.eqsat.metadata.EGraphWithMetadata.

NodeT

The type of nodes in the e-graph.

Value parameters

areEquivalent

A predicate for determining whether two trees are considered the same.

extractor

A mechanism for extracting a foresight.eqsat.Tree from an e-graph at a given root.

getRoot

A function that extracts the foresight.eqsat.EClassCall representing the current root of the e-graph.

setRoot

A function that inserts a new tree root into an e-graph.

transform

The core transformation strategy to apply before rebasing.

Attributes

Companion
object
Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait Strategy[NodeT, EGraphT, (Data, Option[Tree[NodeT]])]
class Object
trait Matchable
class Any
Show all

Members list

Value members

Concrete methods

override def apply(egraph: EGraphT, data: (Data, Option[Tree[NodeT]]), parallelize: ParallelMap): (Option[EGraphT], (Data, Option[Tree[NodeT]]))

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 None if the strategy did not make any changes to the e-graph.

Definition Classes
override def initialData: (Data, Option[Tree[NodeT]])

The initial data for the strategy's first iteration.

The initial data for the strategy's first iteration.

Attributes

Definition Classes

Inherited methods

final def apply(egraph: EGraphT, parallelize: ParallelMap): Option[EGraphT]

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 None if the strategy did not make any changes to the e-graph.

Inherited from:
Strategy
final def dropData: Strategy[NodeT, EGraphT, Unit]

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
def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product
final def repeatUntilStable: Strategy[NodeT, EGraphT, Unit]

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
final def repeatUntilStableWithState: Strategy[NodeT, EGraphT, (Data, Option[Tree[NodeT]])]

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
final def thenApply[Data2](other: Strategy[NodeT, EGraphT, Data2]): Strategy[NodeT, EGraphT, ((Data, Option[Tree[NodeT]]), Data2)]

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
final def withChangeLogger(logChange: (EGraphT, EGraphT) => Unit): Strategy[NodeT, EGraphT, (Data, Option[Tree[NodeT]])]

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
final def withIterationLimit(limit: Option[Int]): Strategy[NodeT, EGraphT, ((Data, Option[Tree[NodeT]]), Int)]

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
final def withIterationLimit(limit: Int): Strategy[NodeT, EGraphT, ((Data, Option[Tree[NodeT]]), Int)]

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
final def withRoot: Strategy[NodeT, EGraphWithRoot[NodeT, EGraphT], (Data, Option[Tree[NodeT]])]

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
final def withTimeout(timeout: Option[Duration]): Strategy[NodeT, EGraphT, ((Data, Option[Tree[NodeT]]), Duration)]

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
final def withTimeout(timeout: Duration): Strategy[NodeT, EGraphT, ((Data, Option[Tree[NodeT]]), Duration)]

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