Crate egg_sketches

egg-sketches is a library adding support for program sketches on top of the egg (e-graphs good) library, an e-graph library optimized for equality saturation.

Sketches are program patterns that are satisfied by a family of programs. They can also be seen as incomplete or partial programs as they can leave details unspecified.

This library is born from our paper on Sketch-Guided Equality Saturation, a semi-automatic technique that allows programmers to provide program sketches to guide rewriting.

If you’re new to egg, e-graphs or equality saturation, the egg tutorial is good to get started.

To see examples of how to use this sketch libary, you can look at the tests on Github.

Modules

recursive_extract

Alternative recursive descent implementation of sketch extraction inspired from pattern matching. This is instead of the bottom-up e-class analysis approach.

util

Utility functions for integration tests and examples

Enums

SketchNode

The language of Sketches.

Functions

eclass_extract_sketch

Returns the best program satisfying s according to cost_f that is represented in the id e-class of egraph, if it exists.

eclass_satisfies_sketch

Is the id e-class of egraph representing at least one program satisfying s?

satisfies_sketch

Returns the set of e-classes of egraph that represent at least one program satisfying s.

Type Aliases

Sketch

A Sketch is a program pattern that is satisfied by a family of programs.