egraphs-good / eggcc

MIT License
42 stars 8 forks source link

DeepCopy doesn't saturate when there are cycles #274

Closed oflatt closed 7 months ago

oflatt commented 8 months ago

Example test:

#[test]
fn test_deep_copy_terminates() -> Result<(), egglog::Error> {
    let build = "
(let id1 (Id (i64-fresh!)))
(let id-outer (Id (i64-fresh!)))
(let loop 
  (Loop id1
    (UnitExpr id-outer)
    (All (Parallel) (Pair (Boolean id1 false) (Num id1 0)))))
(ExprIsValid loop)
;; The loop is equivalent to zero, so the following holds:
(union (Num id1 0)
       (DeepCopyExpr
        (Loop id1
          (UnitExpr id1)
          (All (Parallel) (Pair (Boolean id1 false) (Num id1 0))))
        (Id (i64-fresh!))))
    ";
    let check = "
    ";
    crate::run_test(build, check)
}
oflatt commented 8 months ago

This test is not valid, because the deep copied loop inputs refer to the outer id instead of id1. We think perhaps inputs referring to ids prevents cycles

oflatt commented 8 months ago

I've now modified the example so that the inputs are valid, and we still create a cycle.

oflatt commented 7 months ago

Closing for now- I prefer we never use deep copy