eytans / easter-egg Goto Github PK
View Code? Open in Web Editor NEWThis project forked from egraphs-good/egg
easter egg is a flexible, high-performance e-graph library with support of multiple additional assumptions at once
License: MIT License
This project forked from egraphs-good/egg
easter egg is a flexible, high-performance e-graph library with support of multiple additional assumptions at once
License: MIT License
Try using the colored memo built during congruence_closure for each color?
We need to understand the overhead (memory and runtime) of each color. We should check how many nodes each color has, how many nodes are shared, and how much size does the colored memo take during rebuild. The last one is important to see if we want to hold a memo for a color continually.
We should also collect data on how many black IDs (size of the sets of union_map
) each color has (could help with early stopping).
Currently when we sort parents or nodes we need to clone each node (to be able to use it as a sorting key). We can overcome this by using the "permutations" crate. This will complicate the API a bit, so we should first check how much of an overhead the cloning takes.
The matches should be where they can pass the predicate with an additional color, but can not with a normal match
check_colored
now returns for which colors the condition holds. This means we need to "apply" the Applier
on a colored substitution. We also might need to update the Subst
assignments according to the color. I already did a quick fix, but we need to have tests for this.
Because we separated colored_parents edges from parents #5 , during rebuild we do not canonize colored parents and update the memo. To solve this we need to do a special pass over the colored_parents, but because they do not affect the black merges we should do it only after finishing the classic rebuild.
Doing this will require another loop of
parents.sort
parents.dedup_by(<some color and to_union maintenance>)
update to_do list
But here the unions should only be colored. We should verify that it is safe to merge duplicate nodes for all colors where they appeard (and then delete one of the classes from black - which should happen by colored_rebuild at that point)
Currently the colored pattern implementation (colored_machine) uses a simple modification to the old machine to add branching to each color. This is inefficient when an edge is colored.
Because some edges are colored we can skip them for some colors during matching.
Currently the machine takes all nodes and filters by node color when relevant.
Instead, we need to change how the machine is implemented, pulling "up" the node matching, and then choosing colors by node.
In process unions we are repeating the pattern of
todo.drain:
sort parents
dedup parents and update metadata
union everything
This pattern repeats itself a few time during process_unions
and colored_process_unions
and for memo in some places.
Currently it is implemented for each case separately as the typing of each case differs a bit. We should find a way to generalize the types and dedup closures to a single framework. It will be extra difficult to maintain performance because in process_unions
we are usin Vec::dedup_by
which is more efficient then rebuilding the vector, but in process_colored_unions
we use an iterator.
I want to separate colored parents from normal parents. This can be useful when implementing other features (such as removing nodes #2 ), and might be used to improve efficiency. This is also good for memory use because we only hold colors for colored parents (which have dense colors).
Because parents are only used in rebuilding, and color rebuild needs to recreate parents each time it is not expensive to implement.
I changed the EGraph API to use search
, search_eclass
, and colored_search_eclass
. Each has different assumptions, but in general search
should also return colored results. Therefor, it should jump to colored equivalences from the first eclass we are searching in.
Should also check what are the assumptions for colored_search_eclass
, and add tests accordingly.
When adding a colored edge or a black edge, and some colored edge needs to be modified (i.e. added a color or blackened) we can't update sparse node colors (because at this point the class.nodes is not ordered). Instead we should keep a lazy dirty_colors
list to be used during class rebuild.
This list does not need to contain updates that happened during parent merging because the appropriate edges are also in class.nodes
and will be deduped at rebuild_classes
.
Note: We need to update the nodes in dirty_colors
before applying it.
Currently we implemented (now in features/multi_colored_splits
) the Colored EGraph with edge sharing between different colors. This lead to a lot of overhead in code during the rebuild to manage parents with colors (also compute overhead), or colored_parents
and dirty_colors
. In both cases we save some memory (which is hard to amount theoretically, best case is save all colored_nodes from all colors except one, worst case is none), but at the cost of compute during add
and rebuild
.
The really bad thing about this, is how insurmountable the implementation and accompanying data-structure invariants became.
We will now attempt something a bit different. We will allow only up to a single color for each EClass
, and if it is colored it will have only one node (this might change in the future).
This will enable a massive simplification of the rebuild
process because we will not need to have dirty_colors
(which are used to update the set of colors applicable to a single edge). This means we will only have a single loop of parent deduplication (i.e. finding congruence closure unions) for black, and for colored equality relations.
An additional optimization is mentioned in #14 .
TODO: is it allowed to have more then one colored edge in a colored EClass
(might need to change invariants accordingly).
To do this the data structure will need to change to support a few different things:
memo
and create a separate colored_memo
that can have multiple equal edges (for each color)dirty_colors
EClass
and filter by it during search and rebuild.colored_memo
)colored_process_unions
to include only de-duplication by memo and parents ++ colored_parents
(no need to canonize colored_parents
separately)colored_parents
should be keyed by color (should probably use a hashmap).colored_add
accordingly.union
and colored_union
accordingly.This will have the following invariants:
EClass
s nodes are canonized to said colorparents
always leads to uncolored classes.colored_parents
always leads to colored classes.colored_memo
key are canonized to colored equality relationcolored_memo
values (id's) are the black representative (the node should sit in that class, and it should be colored).In rust, std::mem::discriminant returns a valid value for only 'Enum's. This is ineffective for dynamic languages. All the code relying on the "EClass" being sorted by discriminant should be changed to use a function defined as part of the language (which can be discriminant by default) which will greatly increase runtime for SymbolLang style languages.
Collect benchmarks from unsat
formulas. Translate formulas to terms and "forall" expressions to rewrite rules.
Blocked by #7.
We should add a mechanism to detect bad "colors". We can say a color is bad if it has proven something that can not be. Colors are implemented under the assumption that only a few colored unions will happen, but when we add a false assumption it can imply that false = true
, and the entire E-Graph can fold into a single E-Class which will be very expensive.
The test case in TheSy splits a non-recursive boolean datatype with the function And, Or, and Not. When looking at the splits it finds many seem unnecessary, so we should take a look and improve the split finders if possible.
This is probably due to colored_add
's complexity being factorial in the amount of black_ids of it's children nodes.
We should consider letting colored_add
add uneeded nodes that will be deleted during rebuild.
It seems adding and combinatorically looking for black edges is expensive. One proposed solution is to have a separate place for each colored edge. This way can add a colored edge in its colored canonical form, and if it has a black form delete it during rebuild.
We also want to keep a set of colored edges already added. The set is important because we might later delete an edge during rebuild, but add it again in a new iteration of rewriting.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.