tmp

Author: saulshanabrook

docs/reference/python-integration.md

@@ -679,6 +679,71 @@ r = ruleset(
 egraph.saturate(r)
 ```
 
+## Debugging and Inspection
+
+When a rewrite or rule causes an unexpected equality, these hooks are the fastest ways to
+figure out which rules fired and what the e-graph contains.
+
+### Run reports and rule counts
+
+`EGraph.run(...)` returns a `RunReport` that includes counts and timings per rule.
+
+```{code-cell} python
+egraph = EGraph()
+egraph.register(Math(2) + Math(100))
+report = egraph.run(3, ruleset=ruleset(rewrite(Math(2) + Math(100)).to(Math(102))))
+
+# How many times each rule matched in this run:
+report.num_matches_per_rule
+
+# Total time spent searching/applying each rule:
+report.search_and_apply_time_per_rule
+```
+
+You can also retrieve cumulative stats for the current e-graph:
+
+```{code-cell} python
+egraph = EGraph()
+egraph.register(Math(1) + Math(2))
+egraph.run(2)
+stats = egraph.stats()
+stats.num_matches_per_rule
+```
+
+### Serialize the e-graph
+
+If you create the e-graph with `save_egglog_string=True`, you can dump the program
+sent to egglog for offline inspection or minimization:
+
+```{code-cell} python
+egraph = EGraph(save_egglog_string=True)
+egraph.register(Math(1) + Math(2))
+egraph.run(2)
+egglog_program = egraph.as_egglog_string
+```
+
+For structural inspection, the internal serializer can be used to produce JSON or
+Graphviz output. These are especially useful when an unsound rewrite merges
+unexpected e-classes.
+
+```{code-cell} python
+egraph = EGraph()
+egraph.register(Math(1) + Math(2))
+egraph.run(2)
+serialized = egraph._serialize(split_primitive_outputs=True)  # internal helper
+json_blob = serialized.to_json()
+dot = serialized.to_dot()
+```
+
+### Common pitfalls (rule authoring)
+
+- Primitive container sorts like `Vec[...]` should not be merged or unioned. Avoid
+  using merge functions that combine Vec outputs, and prefer one-way `set_` rules.
+- Guard vector indexing rules with bounds checks (`0 <= k < vs.length()`) to avoid
+  `vec-get failed` panics and unsound conclusions.
+- Be careful with rules that build terms with negative lengths (e.g., `length - 1`);
+  ensure they only fire when the length is proven positive.
+
 ## Custom Cost Models
 
 By default, when extracting from the e-graph, we use a simple cost model, that looks at the costs assigned to each

python/egglog/exp/array_api.py

@@ -766,7 +766,7 @@ def _tuple_int(
     yield rewrite(TupleInt.fn(i2, idx_fn)[i]).to(idx_fn(check_index(i, i2)))
 
     yield rewrite(TupleInt(vs).length()).to(Int(vs.length()))
-    yield rewrite(TupleInt(vs)[Int(k)]).to(vs[k])
+    yield rewrite(TupleInt(vs)[Int(k)]).to(vs[k], k >= 0, k < vs.length())
 
     yield rewrite(TupleInt.fn(Int(k), idx_fn), subsume=True).to(TupleInt(k.range().map(lambda i: idx_fn(Int(i)))))
 
@@ -872,7 +872,7 @@ def _tuple_tuple_int(
     yield rewrite(TupleTupleInt.fn(i2, idx_fn)[i]).to(idx_fn(check_index(i, i2)))
 
     yield rewrite(TupleTupleInt(vs).length()).to(Int(vs.length()))
-    yield rewrite(TupleTupleInt(vs)[Int(k)]).to(vs[k])
+    yield rewrite(TupleTupleInt(vs)[Int(k)]).to(vs[k], k >= 0, k < vs.length())
 
     yield rewrite(TupleTupleInt.fn(Int(k), idx_fn), subsume=True).to(
         TupleTupleInt(k.range().map(lambda i: idx_fn(Int(i))))
@@ -1221,7 +1221,7 @@ def _tuple_value(
     yield rewrite(TupleValue.fn(i2, idx_fn)[i]).to(idx_fn(check_index(i, i2)))
 
     yield rewrite(TupleValue(vs).length()).to(Int(vs.length()))
-    yield rewrite(TupleValue(vs)[Int(k)]).to(vs[k])
+    yield rewrite(TupleValue(vs)[Int(k)]).to(vs[k], k >= 0, k < vs.length())
 
     yield rewrite(TupleValue.fn(Int(k), idx_fn), subsume=True).to(TupleValue(k.range().map(lambda i: idx_fn(Int(i)))))
 
@@ -1266,7 +1266,7 @@ def _tuple_tuple_value(
     yield rewrite(TupleTupleValue.fn(i2, idx_fn)[i]).to(idx_fn(check_index(i, i2)))
 
     yield rewrite(TupleTupleValue(vs).length()).to(Int(vs.length()))
-    yield rewrite(TupleTupleValue(vs)[Int(k)]).to(vs[k])
+    yield rewrite(TupleTupleValue(vs)[Int(k)]).to(vs[k], k >= 0, k < vs.length())
 
     yield rewrite(TupleTupleValue.fn(Int(k), idx_fn), subsume=True).to(
         TupleTupleValue(k.range().map(lambda i: idx_fn(Int(i))))
@@ -1741,7 +1741,7 @@ def _tuple_ndarray(
     yield rewrite(TupleNDArray.fn(i2, idx_fn)[i]).to(idx_fn(check_index(i, i2)))
 
     yield rewrite(TupleNDArray(vs).length()).to(Int(vs.length()))
-    yield rewrite(TupleNDArray(vs)[Int(k)]).to(vs[k])
+    yield rewrite(TupleNDArray(vs)[Int(k)]).to(vs[k], k >= 0, k < vs.length())
 
     yield rewrite(TupleNDArray.fn(Int(k), idx_fn), subsume=True).to(
         TupleNDArray(k.range().map(lambda i: idx_fn(Int(i))))
@@ -2486,8 +2486,11 @@ def _get_current_egraph() -> EGraph:
 
 def try_evaling(egraph: EGraph, schedule: Schedule, expr: Expr, prim_expr: BuiltinExpr) -> Any:
     """
-    Try evaling the expression that will result in a primitive expression being fill.
-    if it fails, display the egraph and raise an error.
+    Try evaluating an expression that should produce a primitive (e.g., Bool/i64).
+    If extraction fails, register the expr, run the schedule, and retry.
+    On egglog panics we dump the .egg program for debugging.
+    A common failure mode is that no rule ever sets the primitive output
+    (e.g., `Boolean.to_bool` / `Int.to_i64`), so extraction fails.
     """
     try:
         return egraph.extract(prim_expr).value  # type: ignore[attr-defined]