From adf78f4307441c49d46f4cefde836d9e683004e4 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 23 Dec 2025 02:20:15 +0000 Subject: [PATCH 1/6] Initial plan From 6c83939743933d135bbfd044cd6d077d40a16b81 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 23 Dec 2025 02:28:20 +0000 Subject: [PATCH 2/6] Add variable support tests for egg Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- tests/test_egg.py | 165 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) diff --git a/tests/test_egg.py b/tests/test_egg.py index d1dd1dc..cabb333 100644 --- a/tests/test_egg.py +++ b/tests/test_egg.py @@ -198,3 +198,168 @@ async def test_egg_cancellation(temp_db): await task except asyncio.CancelledError: pass + + +# Variable-based tests +@pytest.mark.asyncio +async def test_egg_symmetry_with_variables(temp_db): + """Test symmetry with variables: given a(`x)=b(`x) and idea b(t)=a(t), should produce b(t)=a(t).""" + addr, engine, session = temp_db + + # Add fact a(`x)=b(`x) with variable + async with session() as sess: + sess.add(Facts(data="----\n(binary == (unary a `x) (unary b `x))\n")) + sess.add(Ideas(data="----\n(binary == (unary b t) (unary a t))\n")) + await sess.commit() + + # Run the main function with a timeout + task = asyncio.create_task(main(addr, engine, session)) + await asyncio.sleep(0.3) + task.cancel() + try: + await task + except asyncio.CancelledError: + pass + + # Verify that fact b(t)=a(t) was produced + async with session() as sess: + facts = await sess.scalars(select(Facts)) + fact_data = [f.data for f in facts.all()] + assert "----\n(binary == (unary b t) (unary a t))\n" in fact_data + + +@pytest.mark.asyncio +async def test_egg_transitivity_with_variables(temp_db): + """Test transitivity with variables: given a(`x)=b(`x), b(`x)=c(`x), should produce a(t)=c(t).""" + addr, engine, session = temp_db + + # Add facts a(`x)=b(`x) and b(`x)=c(`x) + async with session() as sess: + sess.add(Facts(data="----\n(binary == (unary a `x) (unary b `x))\n")) + sess.add(Facts(data="----\n(binary == (unary b `x) (unary c `x))\n")) + sess.add(Ideas(data="----\n(binary == (unary a t) (unary c t))\n")) + await sess.commit() + + # Run the main function + task = asyncio.create_task(main(addr, engine, session)) + await asyncio.sleep(0.3) + task.cancel() + try: + await task + except asyncio.CancelledError: + pass + + # Verify that fact a(t)=c(t) was produced + async with session() as sess: + facts = await sess.scalars(select(Facts)) + fact_data = [f.data for f in facts.all()] + assert "----\n(binary == (unary a t) (unary c t))\n" in fact_data + + +@pytest.mark.asyncio +async def test_egg_congruence_with_variables(temp_db): + """Test congruence with variables: given x=y, expect f(`z, x)=f(`z, y).""" + addr, engine, session = temp_db + + # Add fact x=y and idea f(`z, x)=f(`z, y) + async with session() as sess: + sess.add(Facts(data="----\n(binary == x y)\n")) + sess.add(Ideas(data="----\n(binary == (binary f `z x) (binary f `z y))\n")) + await sess.commit() + + # Run the main function + task = asyncio.create_task(main(addr, engine, session)) + await asyncio.sleep(0.3) + task.cancel() + try: + await task + except asyncio.CancelledError: + pass + + # Verify that fact was produced + async with session() as sess: + facts = await sess.scalars(select(Facts)) + fact_data = [f.data for f in facts.all()] + assert "----\n(binary == (binary f `z x) (binary f `z y))\n" in fact_data + + +@pytest.mark.asyncio +async def test_egg_substitution_with_variables(temp_db): + """Test substitution with variables: given f(`x) and x=y, expect f(y) can be satisfied.""" + addr, engine, session = temp_db + + # Add fact f(`x) and x=y, then idea f(y) + async with session() as sess: + sess.add(Facts(data="----\n(unary f `x)\n")) + sess.add(Facts(data="----\n(binary == x y)\n")) + sess.add(Ideas(data="----\n(unary f y)\n")) + await sess.commit() + + # Run the main function + task = asyncio.create_task(main(addr, engine, session)) + await asyncio.sleep(0.3) + task.cancel() + try: + await task + except asyncio.CancelledError: + pass + + # Verify that the idea was satisfied + async with session() as sess: + facts = await sess.scalars(select(Facts)) + fact_data = [f.data for f in facts.all()] + assert "----\n(unary f y)\n" in fact_data + + +@pytest.mark.asyncio +async def test_egg_complex_situation_with_variables(temp_db): + """Test comprehensive combination with variables. + + Given: + - a(`x)=b(`x) (fact with variable) + - b(`x)=c(`x) (fact with same variable) + - f(a) (fact) + + Should derive: + - b(t)=a(t) (via symmetry from a(`x)=b(`x)) + - a(t)=c(t) (via transitivity from a(`x)=b(`x), b(`x)=c(`x)) + - f(b)=f(c) (via congruence from b=c, which needs b=c as a separate fact) + - f(c) (via substitution: f(a) and a=c) + """ + addr, engine, session = temp_db + + # Add facts with variables and concrete facts for congruence + async with session() as sess: + sess.add(Facts(data="----\n(binary == (unary a `x) (unary b `x))\n")) + sess.add(Facts(data="----\n(binary == (unary b `x) (unary c `x))\n")) + sess.add(Facts(data="----\n(binary == a b)\n")) # Also add concrete equality for congruence + sess.add(Facts(data="----\n(binary == b c)\n")) # Also add concrete equality for congruence + sess.add(Facts(data="----\n(unary f a)\n")) + # Ideas to test + sess.add(Ideas(data="----\n(binary == (unary b t) (unary a t))\n")) # symmetry + sess.add(Ideas(data="----\n(binary == (unary a t) (unary c t))\n")) # transitivity + sess.add(Ideas(data="----\n(binary == (unary f b) (unary f c))\n")) # congruence + sess.add(Ideas(data="----\n(unary f c)\n")) # substitution + await sess.commit() + + # Run the main function + task = asyncio.create_task(main(addr, engine, session)) + await asyncio.sleep(0.3) + task.cancel() + try: + await task + except asyncio.CancelledError: + pass + + # Verify that all expected facts were produced + async with session() as sess: + facts = await sess.scalars(select(Facts)) + fact_data = [f.data for f in facts.all()] + # Test symmetry: a(`x)=b(`x) should derive b(t)=a(t) + assert "----\n(binary == (unary b t) (unary a t))\n" in fact_data + # Test transitivity: a(`x)=b(`x), b(`x)=c(`x) should derive a(t)=c(t) + assert "----\n(binary == (unary a t) (unary c t))\n" in fact_data + # Test congruence: b=c should derive f(b)=f(c) + assert "----\n(binary == (unary f b) (unary f c))\n" in fact_data + # Test substitution: f(a) and a=c should derive f(c) + assert "----\n(unary f c)\n" in fact_data From 8182c72ff01a080ce44a9173da4d066797ec018f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 23 Dec 2025 02:29:54 +0000 Subject: [PATCH 3/6] Improve documentation for complex test with variables Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- tests/test_egg.py | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/tests/test_egg.py b/tests/test_egg.py index cabb333..221be86 100644 --- a/tests/test_egg.py +++ b/tests/test_egg.py @@ -313,27 +313,33 @@ async def test_egg_substitution_with_variables(temp_db): @pytest.mark.asyncio async def test_egg_complex_situation_with_variables(temp_db): - """Test comprehensive combination with variables. + """Test comprehensive combination with variables alongside concrete facts. + This test demonstrates that variable facts and concrete facts can work together. + Given: - - a(`x)=b(`x) (fact with variable) - - b(`x)=c(`x) (fact with same variable) - - f(a) (fact) + - a(`x)=b(`x) (variable fact: establishes parametric equality) + - b(`x)=c(`x) (variable fact: establishes parametric equality) + - a=b (concrete fact: needed for congruence to work on concrete terms) + - b=c (concrete fact: needed for congruence to work on concrete terms) + - f(a) (concrete fact) Should derive: - - b(t)=a(t) (via symmetry from a(`x)=b(`x)) - - a(t)=c(t) (via transitivity from a(`x)=b(`x), b(`x)=c(`x)) - - f(b)=f(c) (via congruence from b=c, which needs b=c as a separate fact) - - f(c) (via substitution: f(a) and a=c) + - b(t)=a(t) (via symmetry from variable fact a(`x)=b(`x)) + - a(t)=c(t) (via transitivity from variable facts a(`x)=b(`x), b(`x)=c(`x)) + - f(b)=f(c) (via congruence from concrete facts a=b, b=c) + - f(c) (via substitution: f(a) and concrete transitivity a=b=c) """ addr, engine, session = temp_db - # Add facts with variables and concrete facts for congruence + # Add both variable facts and concrete facts async with session() as sess: + # Variable facts for testing parametric reasoning sess.add(Facts(data="----\n(binary == (unary a `x) (unary b `x))\n")) sess.add(Facts(data="----\n(binary == (unary b `x) (unary c `x))\n")) - sess.add(Facts(data="----\n(binary == a b)\n")) # Also add concrete equality for congruence - sess.add(Facts(data="----\n(binary == b c)\n")) # Also add concrete equality for congruence + # Concrete facts needed for congruence on non-parametric terms + sess.add(Facts(data="----\n(binary == a b)\n")) + sess.add(Facts(data="----\n(binary == b c)\n")) sess.add(Facts(data="----\n(unary f a)\n")) # Ideas to test sess.add(Ideas(data="----\n(binary == (unary b t) (unary a t))\n")) # symmetry @@ -359,7 +365,7 @@ async def test_egg_complex_situation_with_variables(temp_db): assert "----\n(binary == (unary b t) (unary a t))\n" in fact_data # Test transitivity: a(`x)=b(`x), b(`x)=c(`x) should derive a(t)=c(t) assert "----\n(binary == (unary a t) (unary c t))\n" in fact_data - # Test congruence: b=c should derive f(b)=f(c) + # Test congruence: a=b, b=c should derive f(b)=f(c) assert "----\n(binary == (unary f b) (unary f c))\n" in fact_data - # Test substitution: f(a) and a=c should derive f(c) + # Test substitution: f(a) and a=b=c should derive f(c) assert "----\n(unary f c)\n" in fact_data From 82d5b8ca3eee60a1b4863018832f7ba293757270 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 23 Dec 2025 02:31:18 +0000 Subject: [PATCH 4/6] Improve docstrings for variable test clarity Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- tests/test_egg.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/test_egg.py b/tests/test_egg.py index 221be86..5a1eef1 100644 --- a/tests/test_egg.py +++ b/tests/test_egg.py @@ -203,7 +203,9 @@ async def test_egg_cancellation(temp_db): # Variable-based tests @pytest.mark.asyncio async def test_egg_symmetry_with_variables(temp_db): - """Test symmetry with variables: given a(`x)=b(`x) and idea b(t)=a(t), should produce b(t)=a(t).""" + """Test symmetry with variables: given variable equality a(`x)=b(`x), + the system can derive the symmetric concrete instance b(t)=a(t) by + unifying the variable pattern with concrete value t.""" addr, engine, session = temp_db # Add fact a(`x)=b(`x) with variable @@ -285,7 +287,9 @@ async def test_egg_congruence_with_variables(temp_db): @pytest.mark.asyncio async def test_egg_substitution_with_variables(temp_db): - """Test substitution with variables: given f(`x) and x=y, expect f(y) can be satisfied.""" + """Test substitution with variables: given fact f(`x) with a variable argument + and equality x=y, the system can derive f(y) by unifying the variable pattern + f(`x) with f(y) where `x matches y, then checking if the resulting equality holds.""" addr, engine, session = temp_db # Add fact f(`x) and x=y, then idea f(y) From 958977ca18f3c2a1759cd8e58e2a37db2d48e8d9 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 23 Dec 2025 02:43:56 +0000 Subject: [PATCH 5/6] Fix congruence and substitution tests per reviewer feedback MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Congruence test now correctly tests: a(`x)=b(`x) → f(a(t))=f(b(t)) - Substitution test now correctly tests: f(a(`x)), a(`x)=b(`x) → f(b(t)) Both tests now use nested function applications as intended Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- tests/test_egg.py | 48 ++++++++++++++++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 15 deletions(-) diff --git a/tests/test_egg.py b/tests/test_egg.py index 5a1eef1..1467cdb 100644 --- a/tests/test_egg.py +++ b/tests/test_egg.py @@ -260,13 +260,20 @@ async def test_egg_transitivity_with_variables(temp_db): @pytest.mark.asyncio async def test_egg_congruence_with_variables(temp_db): - """Test congruence with variables: given x=y, expect f(`z, x)=f(`z, y).""" + """Test congruence with variables: given a(`x)=b(`x), derive f(a(t))=f(b(t)). + + This tests that variable patterns enable congruence on nested structures: + - Variable fact a(`x)=b(`x) allows deriving concrete equality a(t)=b(t) + - Concrete equality a(t)=b(t) enables congruence to derive f(a(t))=f(b(t)) + """ addr, engine, session = temp_db - # Add fact x=y and idea f(`z, x)=f(`z, y) + # Add variable equality fact async with session() as sess: - sess.add(Facts(data="----\n(binary == x y)\n")) - sess.add(Ideas(data="----\n(binary == (binary f `z x) (binary f `z y))\n")) + sess.add(Facts(data="----\n(binary == (unary a `x) (unary b `x))\n")) + # Add ideas to test the derivation chain + sess.add(Ideas(data="----\n(binary == (unary a t) (unary b t))\n")) # concrete instance + sess.add(Ideas(data="----\n(binary == (unary f (unary a t)) (unary f (unary b t)))\n")) # congruence await sess.commit() # Run the main function @@ -278,25 +285,33 @@ async def test_egg_congruence_with_variables(temp_db): except asyncio.CancelledError: pass - # Verify that fact was produced + # Verify that both facts were produced async with session() as sess: facts = await sess.scalars(select(Facts)) fact_data = [f.data for f in facts.all()] - assert "----\n(binary == (binary f `z x) (binary f `z y))\n" in fact_data + # First, a(t)=b(t) should be derived from a(`x)=b(`x) + assert "----\n(binary == (unary a t) (unary b t))\n" in fact_data + # Then, f(a(t))=f(b(t)) should be derived via congruence + assert "----\n(binary == (unary f (unary a t)) (unary f (unary b t)))\n" in fact_data @pytest.mark.asyncio async def test_egg_substitution_with_variables(temp_db): - """Test substitution with variables: given fact f(`x) with a variable argument - and equality x=y, the system can derive f(y) by unifying the variable pattern - f(`x) with f(y) where `x matches y, then checking if the resulting equality holds.""" + """Test substitution with variables: given f(a(`x)) and a(`x)=b(`x), derive f(b(t)). + + This tests that variable patterns enable substitution in nested structures: + - Facts f(a(`x)) and a(`x)=b(`x) allow deriving f(b(`x)) via e-graph equality + - Variable fact f(b(`x)) allows deriving concrete instance f(b(t)) + """ addr, engine, session = temp_db - # Add fact f(`x) and x=y, then idea f(y) + # Add facts with variables async with session() as sess: - sess.add(Facts(data="----\n(unary f `x)\n")) - sess.add(Facts(data="----\n(binary == x y)\n")) - sess.add(Ideas(data="----\n(unary f y)\n")) + sess.add(Facts(data="----\n(unary f (unary a `x))\n")) + sess.add(Facts(data="----\n(binary == (unary a `x) (unary b `x))\n")) + # Add ideas to test the derivation chain + sess.add(Ideas(data="----\n(unary f (unary b `x))\n")) # substitution via equality + sess.add(Ideas(data="----\n(unary f (unary b t))\n")) # concrete instance await sess.commit() # Run the main function @@ -308,11 +323,14 @@ async def test_egg_substitution_with_variables(temp_db): except asyncio.CancelledError: pass - # Verify that the idea was satisfied + # Verify that both facts were produced async with session() as sess: facts = await sess.scalars(select(Facts)) fact_data = [f.data for f in facts.all()] - assert "----\n(unary f y)\n" in fact_data + # First, f(b(`x)) should be derived via substitution + assert "----\n(unary f (unary b `x))\n" in fact_data + # Then, f(b(t)) should be derived as a concrete instance + assert "----\n(unary f (unary b t))\n" in fact_data @pytest.mark.asyncio From 683fd07657c95d94fc93f97e3d0bd071861b725e Mon Sep 17 00:00:00 2001 From: Hao Zhang Date: Tue, 23 Dec 2025 10:50:09 +0800 Subject: [PATCH 6/6] run pre-commit hook. --- tests/test_egg.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/test_egg.py b/tests/test_egg.py index 1467cdb..ceb60dc 100644 --- a/tests/test_egg.py +++ b/tests/test_egg.py @@ -203,8 +203,8 @@ async def test_egg_cancellation(temp_db): # Variable-based tests @pytest.mark.asyncio async def test_egg_symmetry_with_variables(temp_db): - """Test symmetry with variables: given variable equality a(`x)=b(`x), - the system can derive the symmetric concrete instance b(t)=a(t) by + """Test symmetry with variables: given variable equality a(`x)=b(`x), + the system can derive the symmetric concrete instance b(t)=a(t) by unifying the variable pattern with concrete value t.""" addr, engine, session = temp_db @@ -261,7 +261,7 @@ async def test_egg_transitivity_with_variables(temp_db): @pytest.mark.asyncio async def test_egg_congruence_with_variables(temp_db): """Test congruence with variables: given a(`x)=b(`x), derive f(a(t))=f(b(t)). - + This tests that variable patterns enable congruence on nested structures: - Variable fact a(`x)=b(`x) allows deriving concrete equality a(t)=b(t) - Concrete equality a(t)=b(t) enables congruence to derive f(a(t))=f(b(t)) @@ -298,7 +298,7 @@ async def test_egg_congruence_with_variables(temp_db): @pytest.mark.asyncio async def test_egg_substitution_with_variables(temp_db): """Test substitution with variables: given f(a(`x)) and a(`x)=b(`x), derive f(b(t)). - + This tests that variable patterns enable substitution in nested structures: - Facts f(a(`x)) and a(`x)=b(`x) allow deriving f(b(`x)) via e-graph equality - Variable fact f(b(`x)) allows deriving concrete instance f(b(t)) @@ -338,7 +338,7 @@ async def test_egg_complex_situation_with_variables(temp_db): """Test comprehensive combination with variables alongside concrete facts. This test demonstrates that variable facts and concrete facts can work together. - + Given: - a(`x)=b(`x) (variable fact: establishes parametric equality) - b(`x)=c(`x) (variable fact: establishes parametric equality)