Add proof production (egraphs-good#115)

* making progress on interface

* fix up interface again

* minor docs stuff

* undo searchmatch struct

* unions are delayed until rebuild

* refactor much into explain file

* rework justification structure

* big get_ast refactor

* add checking (not passing yet)

* modified rebuilding to maintain congruence before analysis pending

* tests passing!

* implement proof production (untested)

* explanation class

* make math examples call with justification

* printing explanation trees

* various bugs

* make proof checker

* tests passing

* remove confusing comment

* change api for apply_one

* fix subtle bug in lambda example

* fix up congruence for analysis

* some cleanup

* new structure which is better for caching

* Revert "new structure which is better for caching"

This reverts commit 31df99a.

* caching works elegantly!

* run formatting

* disable test for proof production

* add test pass for proof generation

* rename union_roots back to union

* some progress on docs

* more small progress on docs

* document tree and flattened formats minimally

* starting on nits

* a bunch of nits

* fix up rebuilding with analysis and tests

* a better solution to the analysis problem

* docs for string representation

* fix format of example explanations

* rename to get_ast

* disallow calling explanation when feature not enabled

* format

* stray prints

* don't clone asts when you don't need them

* fix up conditional compilation

* fmt

* improve rebuilding with Max

* change rule names to arc

* use cow for the patternasts and thus ascend to a new level of rust development

* simplify unification api greatly

* add let binding to printing explanations

* add documentation for let binding

* make apply_one perform the union to clean up interface

* remove Cow when not needed

* make explain an option

* fix up diff_power_harder

* nits

* add to changelog

* apply_one for pattern faster when explanations off

* simplify analysis rebuilding slightly

* re-implement pattern apply_matches

* oops

* add disabling explanations

* fix up disabling

* working on explanations tutorial

* continue working on tutorial

* more work on tutorial

* tutorial rough draft ready

* also generate sexps

* change simplify_const back oops

* move analysis docs to rightful place

Author: oflatt

CHANGELOG.md

@@ -5,11 +5,23 @@
 ## [Unreleased] - ReleaseDate
 
 ### Added
+- The egraph now has an `EGraph::with_explanations_enabled` mode that allows for
+  explaining why two terms are equivalent in the egraph.
+  In explanations mode, all unions must be done through `union_instantiations` in order
+  to justify the union.
+  Calling `explain_equivalence` returns an `Explanation`
+  which has both a `FlatExplanation` form and a
+  `TreeExplanation` form.
 - The `BackoffScheduler` is now more flexible.
 - `EGraph::pre_union` allows inspection of unions, which can be useful for debugging.
 - The dot printer is now more flexible.
 
 ### Changed
+- All unions are now delayed until rebuilding, so `EGraph::rebuild` be called to observe effects.
+- The `apply_one` function on appliers now needs to perform unions.
+- The congruence closure algorithm now keeps the egraph congruent before
+  doing any analysis (calling `make`). It does this by interleaving rebuilding
+  and doing analysis.
 - `EGraph::add_expr` now proceeds linearly through the given `RecExpr`, which
   should be faster and include _all_ e-nodes from the expression.
 - `Rewrite` now has public `searcher` and `applier` fields and no `long_name`.

Makefile

@@ -4,6 +4,9 @@ all: test nits bench
 test:
 	cargo build --release
 	cargo test --release
+	# don't run examples in proof-production mode
+	EGG_TEST_EXPLANATIONS=true cargo test --lib --bins --tests --benches --release
+	
 
 .PHONY: nits
 nits:
@@ -14,9 +17,14 @@ nits:
 	cargo deadlinks
 
 	cargo clippy --tests
+	EGG_TEST_EXPLANATIONS=true cargo clippy --tests
 	cargo clippy --tests --features "serde-1"
 	cargo clippy --tests --features "reports"
 
 .PHONY: bench
 bench:
 	cargo bench | ./scripts/filter-iai-output.py
+
+.PHONY: bench_explanations
+bench_explanations:
+	EGG_TEST_EXPLANATIONS=true cargo bench | ./scripts/filter-iai-output.py

scripts/filter-iai-output.py

@@ -12,9 +12,11 @@
 ratios = []
 
 for line in fileinput.input():
-    if match := BENCH_NAME.match(line):
+    match = BENCH_NAME.match(line)
+    if match:
         name = match[1]
-    if match := EST_CYCLES.match(line):
+    match = EST_CYCLES.match(line)
+    if match:
         if not printed_headers:
             printed_headers = True
             print(f'{"name":25} {"cycles":>10} {"diff":>10}')

src/eclass.rs

@@ -13,6 +13,7 @@ pub struct EClass<L, D> {
     pub nodes: Vec<L>,
     /// The analysis data associated with this eclass.
     pub data: D,
+    /// The parent enodes and their original Ids.
     pub(crate) parents: Vec<(L, Id)>,
 }