Algorithm.EqSat.Build

Functions related to building and maintaining e-graphs Heavily based on hegg (https:/github.comalt-romes/hegg by alt-romes)

Documentation

add :: Monad m => CostFun -> ENode -> EGraphST m EClassId

adds a new or existing e-node (merging if necessary)

rebuild :: Monad m => CostFun -> EGraphST m ()

rebuilds the e-graph after inserting or merging e-classes

repair :: Monad m => CostFun -> EClassId -> ENode -> EGraphST m ()

repairs e-node by canonizing its children if the canonized e-node already exists in e-graph, merge the e-classes

repairAnalysis :: Monad m => CostFun -> EClassId -> ENode -> EGraphST m ()

repair the analysis of the e-class considering the new added e-node

merge :: Monad m => CostFun -> EClassId -> EClassId -> EGraphST m EClassId

merge to equivalent e-classes

modifyEClass :: Monad m => CostFun -> EClassId -> EGraphST m EClassId

modify an e-class, e.g., add constant e-node and prune non-leaves

DB

createDB :: Monad m => EGraphST m DB

createDB creates a database of patterns from an e-graph it simply calls addToDB for every pair (e-node, e-class id) from the e-graph.

addToDB :: Monad m => ENode -> EClassId -> EGraphST m ()

addToDB adds an e-node and e-class id to the database

populate :: Maybe IntTrie -> [EClassId] -> Maybe IntTrie

Populates an IntTrie with a sequence of e-class ids

canonizeMap :: Monad m => (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST m (Map ClassOrVar ClassOrVar, ClassOrVar)

applyMatch :: Monad m => CostFun -> Rule -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST m ()

applyMergeOnlyMatch :: Monad m => CostFun -> Rule -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST m ()

classOfENode :: Monad m => CostFun -> Map ClassOrVar ClassOrVar -> Pattern -> EGraphST m (Maybe EClassId)

gets the e-node of the target of the rule TODO: add consts and modify

reprPrat :: Monad m => CostFun -> Map ClassOrVar ClassOrVar -> Pattern -> EGraphST m EClassId

adds the target of the rule into the e-graph

isValidHeight :: Monad m => (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST m Bool

isValidConditions :: Monad m => Condition -> (Map ClassOrVar ClassOrVar, ClassOrVar) -> EGraphST m Bool

returns True if the condition of a rule is valid for that match

Tree to e-graph conversion and utility functions

fromTree :: Monad m => CostFun -> Fix SRTree -> EGraphST m EClassId

Creates an e-graph from an expression tree

fromTrees :: Monad m => CostFun -> [Fix SRTree] -> EGraphST m [EClassId]

Builds an e-graph from multiple independent trees

getBest :: Monad m => EClassId -> EGraphST m (Fix SRTree)

gets the best expression given the default cost function

getExpressionFrom :: Monad m => EClassId -> EGraphST m (Fix SRTree)

returns one expression rooted at e-class eId TODO: avoid loopings

getAllExpressionsFrom :: Monad m => EClassId -> EGraphST m [Fix SRTree]

returns all expressions rooted at e-class eId TODO: check for infinite list

getRndExpressionFrom :: EClassId -> EGraphST (State StdGen) (Fix SRTree)

returns a random expression rooted at e-class eId

cleanMaps :: Monad m => EGraphST m ()

forceState :: Monad m => StateT s m ()