Crate slotted_egraphs

Expand description

Slotted e-graphs are a datastructure for representing congruence relations over terms with variables and binders.

For a higher level introduction to slotted e-graphs, consider

For an example implementation of a Language with binders in slotted e-graphs, consider the RISE implementation in here.

Macros§

bare_language_child: Implements LanguageChildren for payload types that are independent of Slots. For example u32, String etc.
define_language
rw

AppliedId: AppliedIds are invocations of e-classes.
AstSize: The ‘default’ CostFunction. It measures the size of the abstract syntax tree of the corresponding term.
Bind
CongruenceProof
EGraph: A datastructure to efficiently represent congruence relations on terms with binders.
Equation
ExplicitProof
ExtractionSubst: A SubstMethod that extracts the smallest term (measured by AstSize) of an e-class to do substitution on it.
Extractor: An object used for quickly extracting terms (i.e. RecExprs) using a given CostFunction.
Id: Ids identify e-classes.
Iteration
ProgressMeasure: A Progress Measure to check saturation of an e-graph with.
ProvenEqRaw
RecExpr: A “term” or “expression” from some given Language L.
ReflexivityProof
Report
Rewrite: An equational rewrite rule.
RewriteT: Use this type when you want to build your own Rewrite.
Runner
RunnerLimits
Slot: Slots represent Variable names.
SlotMap: A mapping between the parameter-slots of an e-class, and some “invocation” slots that you want to put into them.
Symbol: A interned string in the global symbol table.
SymmetryProof
SynExprSubst: A SubstMethod that uses the EGraph::get_syn_expr of an e-class to do substitution on it.
TransitivityProof

AbstractVecMap: An abstract vec map
AbstractVecSet: An abstract vec set
Analysis: E-Graph Analysis allows you to propagate information upwards through the E-Graph.
Cond
CostFunction: A cost function to guide extraction.
IterationData
Language: A trait to define your Language (i.e. your E-Node type).
LanguageChildren
SubstMethod: Specifies a certain implementation of how substitution b[x := t] is implemented internally.

and
any_to_t
apply_rewrites: Applies each given rewrite rule to the E-Graph once. Returns an indicator for whether the e-graph changed as a result.
ast_size_extract
ematch_all
extract
lookup_rec_expr
not
or
pattern_subst
pattern_to_re
re_to_pattern
run_eqsat
slot_free_in