Skip to content

Instantly share code, notes, and snippets.

@saulshanabrook

saulshanabrook/eqsat-basic.ipynb

Created May 15, 2023 20:16
Show Gist options
  • Save saulshanabrook/b711f6f0f0d0db60aed64bc8da22774f to your computer and use it in GitHub Desktop.
Save saulshanabrook/b711f6f0f0d0db60aed64bc8da22774f to your computer and use it in GitHub Desktop.
Download ZIP
Display the source blob
Display the rendered blob
Raw
eqsat-basic.ipynb
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"id": "7b3486bb-d281-4722-8426-d0dca6e2617e",
"metadata": {
"tags": []
},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 8.0.5 (20230430.1635)\n",
" -->\n",
"<!-- Title: egg_smol Pages: 1 -->\n",
"<svg width=\"636pt\" height=\"276pt\"\n",
" viewBox=\"0.00 0.00 636.00 276.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 272)\">\n",
"<title>egg_smol</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-272 632,-272 632,4 -4,4\"/>\n",
"<g id=\"clust1\" class=\"cluster\">\n",
"<title>cluster_0</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"298,-64 298,-116 454,-116 454,-64 298,-64\"/>\n",
"</g>\n",
"<g id=\"clust2\" class=\"cluster\">\n",
"<title>cluster_5</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"464,-136 464,-188 620,-188 620,-136 464,-136\"/>\n",
"</g>\n",
"<g id=\"clust3\" class=\"cluster\">\n",
"<title>cluster_4</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"44,-208 44,-260 286,-260 286,-208 44,-208\"/>\n",
"</g>\n",
"<g id=\"clust4\" class=\"cluster\">\n",
"<title>cluster_3</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"98,-136 98,-188 256,-188 256,-136 98,-136\"/>\n",
"</g>\n",
"<g id=\"clust7\" class=\"cluster\">\n",
"<title>cluster_1</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"172,-64 172,-116 290,-116 290,-64 172,-64\"/>\n",
"</g>\n",
"<g id=\"clust5\" class=\"cluster\">\n",
"<title>cluster_2</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"8,-64 8,-116 164,-116 164,-64 8,-64\"/>\n",
"</g>\n",
"<g id=\"clust6\" class=\"cluster\">\n",
"<title>cluster_7</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"351,-208 351,-260 591,-260 591,-208 351,-208\"/>\n",
"</g>\n",
"<g id=\"clust8\" class=\"cluster\">\n",
"<title>cluster_6</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"296,-136 296,-188 456,-188 456,-136 296,-136\"/>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"376\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"376\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0_0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"376\" cy=\"-90\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"376\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 0_0&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>0_0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M376,-71.7C376,-64.24 376,-55.32 376,-46.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"379.5,-47.1 376,-37.1 372.5,-47.1 379.5,-47.1\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"542\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"542\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
"</g>\n",
"<!-- 5_0 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>5_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"542\" cy=\"-162\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"542\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 5_0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>5_0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M542,-143.7C542,-136.24 542,-127.32 542,-118.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"545.5,-119.1 542,-109.1 538.5,-119.1 545.5,-119.1\"/>\n",
"</g>\n",
"<!-- 4_0 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"206\" cy=\"-234\" rx=\"72.34\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"206\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____mul__</text>\n",
"</g>\n",
"<!-- 4_0&#45;&gt;0_0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>4_0&#45;&gt;0_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M229,-216.53C239.19,-208.59 250.89,-198.52 260,-188 277.77,-167.49 272.25,-154.61 292,-136 297.53,-130.79 303.78,-126.01 310.31,-121.66\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"311.73,-124.27 318.34,-116 308.01,-118.34 311.73,-124.27\"/>\n",
"</g>\n",
"<!-- 3_0 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>3_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"177\" cy=\"-162\" rx=\"70.8\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"177\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____add__</text>\n",
"</g>\n",
"<!-- 4_0&#45;&gt;3_0 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>4_0&#45;&gt;3_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M198.83,-215.7C195.64,-207.98 191.8,-198.71 188.23,-190.11\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"194.93,-196.12 187.09,-189 188.78,-199.46 194.93,-196.12\"/>\n",
"</g>\n",
"<!-- 1_0 -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>1_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"231\" cy=\"-90\" rx=\"50.84\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"231\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num__var</text>\n",
"</g>\n",
"<!-- 3_0&#45;&gt;1_0 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>3_0&#45;&gt;1_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M190.07,-144.05C196.51,-135.71 204.39,-125.49 211.52,-116.25\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"203.53,-123.46 211.05,-116 200.51,-117.14 203.53,-123.46\"/>\n",
"</g>\n",
"<!-- 2_0 -->\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>2_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"86\" cy=\"-90\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"86\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 3_0&#45;&gt;2_0 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>3_0&#45;&gt;2_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M155.43,-144.41C146.91,-137.85 136.81,-130.09 127,-122.54\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"129.56,-119.32 119.5,-116 125.29,-124.87 129.56,-119.32\"/>\n",
"</g>\n",
"<!-- 4_1 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>4_1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"84\" cy=\"-234\" rx=\"31.9\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"84\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">expr1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node14\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"231\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"231\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">x</text>\n",
"</g>\n",
"<!-- 1_0&#45;&gt;3 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>1_0&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M231,-71.7C231,-64.24 231,-55.32 231,-46.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"234.5,-47.1 231,-37.1 227.5,-47.1 234.5,-47.1\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"86\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"86\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 2_0&#45;&gt;2 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2_0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M86,-71.7C86,-64.24 86,-55.32 86,-46.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.5,-47.1 86,-37.1 82.5,-47.1 89.5,-47.1\"/>\n",
"</g>\n",
"<!-- 7_0 -->\n",
"<g id=\"node11\" class=\"node\">\n",
"<title>7_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"512\" cy=\"-234\" rx=\"70.8\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"512\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____add__</text>\n",
"</g>\n",
"<!-- 7_0&#45;&gt;5_0 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>7_0&#45;&gt;5_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M519.42,-215.7C522.72,-207.98 526.69,-198.71 530.38,-190.11\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"529.45,-199.36 531.67,-189 523.47,-195.71 529.45,-199.36\"/>\n",
"</g>\n",
"<!-- 6_0 -->\n",
"<g id=\"node12\" class=\"node\">\n",
"<title>6_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"376\" cy=\"-162\" rx=\"72.34\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"376\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____mul__</text>\n",
"</g>\n",
"<!-- 7_0&#45;&gt;6_0 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>7_0&#45;&gt;6_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M481.48,-217.29C467.47,-210.08 450.37,-201.28 434.05,-192.88\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"436.06,-189.46 425.57,-188 432.85,-195.69 436.06,-189.46\"/>\n",
"</g>\n",
"<!-- 6_0&#45;&gt;0_0 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>6_0&#45;&gt;0_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M376,-143.7C376,-136.24 376,-127.32 376,-118.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"379.5,-127 376,-117 372.5,-127 379.5,-127\"/>\n",
"</g>\n",
"<!-- 6_0&#45;&gt;1_0 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>6_0&#45;&gt;1_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M343.82,-145.46C328.69,-138.16 310.14,-129.2 292.47,-120.68\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"294.31,-117.19 283.78,-116 291.26,-123.5 294.31,-117.19\"/>\n",
"</g>\n",
"<!-- 7_1 -->\n",
"<g id=\"node13\" class=\"node\">\n",
"<title>7_1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"391\" cy=\"-234\" rx=\"31.9\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"391\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">expr2</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"EGraph()"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"\"\"\"\n",
"Basic equality saturation example.\n",
"==================================\n",
"\"\"\"\n",
"from __future__ import annotations\n",
"\n",
"from egglog import *\n",
"\n",
"egraph = EGraph()\n",
"\n",
"@egraph.class_\n",
"class Num(BaseExpr):\n",
" def __init__(self, value: i64Like) -> None:\n",
" ...\n",
"\n",
" @classmethod\n",
" def var(cls, name: StringLike) -> Num: # type: ignore[empty-body]\n",
" ...\n",
"\n",
" def __add__(self, other: Num) -> Num: # type: ignore[empty-body]\n",
" ...\n",
"\n",
" def __mul__(self, other: Num) -> Num: # type: ignore[empty-body]\n",
" ...\n",
"# expr1 = 2 * (x + 3)\n",
"expr1 = egraph.define(\"expr1\", Num(2) * (Num.var(\"x\") + Num(3)))\n",
"# expr2 = 6 + 2 * x\n",
"expr2 = egraph.define(\"expr2\", Num(6) + Num(2) * Num.var(\"x\"))\n",
"egraph"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "2ecc6726-ec46-4990-8b69-6d583ffe5fb1",
"metadata": {
"tags": []
},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 8.0.5 (20230430.1635)\n",
" -->\n",
"<!-- Title: egg_smol Pages: 1 -->\n",
"<svg width=\"1087pt\" height=\"276pt\"\n",
" viewBox=\"0.00 0.00 1087.00 276.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 272)\">\n",
"<title>egg_smol</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-272 1083,-272 1083,4 -4,4\"/>\n",
"<g id=\"clust5\" class=\"cluster\">\n",
"<title>cluster_1</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"156,-64 156,-116 274,-116 274,-64 156,-64\"/>\n",
"</g>\n",
"<g id=\"clust3\" class=\"cluster\">\n",
"<title>cluster_2</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"282,-64 282,-116 438,-116 438,-64 282,-64\"/>\n",
"</g>\n",
"<g id=\"clust1\" class=\"cluster\">\n",
"<title>cluster_3</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"69,-136 69,-188 387,-188 387,-136 69,-136\"/>\n",
"</g>\n",
"<g id=\"clust4\" class=\"cluster\">\n",
"<title>cluster_0</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"497,-64 497,-116 653,-116 653,-64 497,-64\"/>\n",
"</g>\n",
"<g id=\"clust2\" class=\"cluster\">\n",
"<title>cluster_8</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"595,-136 595,-188 1071,-188 1071,-136 595,-136\"/>\n",
"</g>\n",
"<g id=\"clust6\" class=\"cluster\">\n",
"<title>cluster_6</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"395,-136 395,-188 555,-188 555,-136 395,-136\"/>\n",
"</g>\n",
"<g id=\"clust7\" class=\"cluster\">\n",
"<title>cluster_4</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"8,-208 8,-260 734,-260 734,-208 8,-208\"/>\n",
"</g>\n",
"<!-- 3_0 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>3_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"308\" cy=\"-162\" rx=\"70.8\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"308\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____add__</text>\n",
"</g>\n",
"<!-- 1_0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"215\" cy=\"-90\" rx=\"50.84\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"215\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num__var</text>\n",
"</g>\n",
"<!-- 3_0&#45;&gt;1_0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>3_0&#45;&gt;1_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M285.96,-144.41C277.25,-137.85 266.93,-130.09 256.9,-122.54\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"259.31,-119.21 249.21,-116 255.1,-124.81 259.31,-119.21\"/>\n",
"</g>\n",
"<!-- 2_0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"360\" cy=\"-90\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"360\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 3_0&#45;&gt;2_0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>3_0&#45;&gt;2_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M320.59,-144.05C326.72,-135.8 334.22,-125.7 341.03,-116.54\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"336.29,-126.71 340.53,-117 331.16,-121.95 336.29,-126.71\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node13\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"215\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"215\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">x</text>\n",
"</g>\n",
"<!-- 1_0&#45;&gt;4 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>1_0&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M215,-71.7C215,-64.24 215,-55.32 215,-46.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"218.5,-47.1 215,-37.1 211.5,-47.1 218.5,-47.1\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node11\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"360\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"360\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 2_0&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>2_0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M360,-71.7C360,-64.24 360,-55.32 360,-46.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"363.5,-47.1 360,-37.1 356.5,-47.1 363.5,-47.1\"/>\n",
"</g>\n",
"<!-- 3_1 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>3_1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"148\" cy=\"-162\" rx=\"70.8\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"148\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____add__</text>\n",
"</g>\n",
"<!-- 3_1&#45;&gt;1_0 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>3_1&#45;&gt;1_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M164.22,-144.05C170.14,-137.87 177.04,-130.66 183.82,-123.58\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"185.69,-126.64 190.07,-117 180.63,-121.8 185.69,-126.64\"/>\n",
"</g>\n",
"<!-- 3_1&#45;&gt;2_0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>3_1&#45;&gt;2_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M190.14,-147.09C214.18,-139.15 245.21,-128.9 274.15,-119.35\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"274.89,-122.46 283.29,-116 272.7,-115.81 274.89,-122.46\"/>\n",
"</g>\n",
"<!-- 8_0 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>8_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"675\" cy=\"-162\" rx=\"72.34\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"675\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____mul__</text>\n",
"</g>\n",
"<!-- 8_0&#45;&gt;2_0 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>8_0&#45;&gt;2_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M622.28,-149.28C574.97,-138.77 504.58,-123.13 448.63,-110.69\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"449.52,-107.09 439,-108.33 448,-113.92 449.52,-107.09\"/>\n",
"</g>\n",
"<!-- 0_0 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>0_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"575\" cy=\"-90\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"575\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 8_0&#45;&gt;0_0 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>8_0&#45;&gt;0_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M651.55,-144.59C641.96,-137.87 630.53,-129.87 619.47,-122.13\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"621.91,-118.87 611.71,-116 617.9,-124.6 621.91,-118.87\"/>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node12\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"575\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"575\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0_0&#45;&gt;3 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>0_0&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M575,-71.7C575,-64.24 575,-55.32 575,-46.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"578.5,-47.1 575,-37.1 571.5,-47.1 578.5,-47.1\"/>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"993\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"993\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
"</g>\n",
"<!-- 8_1 -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>8_1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"993\" cy=\"-162\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"993\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 8_1&#45;&gt;0 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>8_1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M993,-143.7C993,-136.24 993,-127.32 993,-118.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"996.5,-119.1 993,-109.1 989.5,-119.1 996.5,-119.1\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"835\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"835\" y=\"-84.95\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
"</g>\n",
"<!-- 8_2 -->\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>8_2</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"835\" cy=\"-162\" rx=\"69.78\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"835\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____init__</text>\n",
"</g>\n",
"<!-- 8_2&#45;&gt;1 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>8_2&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M835,-143.7C835,-136.24 835,-127.32 835,-118.97\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"838.5,-119.1 835,-109.1 831.5,-119.1 838.5,-119.1\"/>\n",
"</g>\n",
"<!-- 6_0 -->\n",
"<g id=\"node14\" class=\"node\">\n",
"<title>6_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"475\" cy=\"-162\" rx=\"72.34\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"475\" y=\"-156.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____mul__</text>\n",
"</g>\n",
"<!-- 6_0&#45;&gt;1_0 -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>6_0&#45;&gt;1_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M432.09,-147.2C418.98,-143.27 404.47,-139.19 391,-136 344.76,-125.06 329.19,-129.23 284.36,-117.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"285.57,-114.07 275,-114.82 283.73,-120.82 285.57,-114.07\"/>\n",
"</g>\n",
"<!-- 6_0&#45;&gt;0_0 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>6_0&#45;&gt;0_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M498.45,-144.59C508.04,-137.87 519.47,-129.87 530.53,-122.13\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"532.1,-124.6 538.29,-116 528.09,-118.87 532.1,-124.6\"/>\n",
"</g>\n",
"<!-- 4_0 -->\n",
"<g id=\"node15\" class=\"node\">\n",
"<title>4_0</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"655\" cy=\"-234\" rx=\"70.8\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"655\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____add__</text>\n",
"</g>\n",
"<!-- 4_0&#45;&gt;8_0 -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>4_0&#45;&gt;8_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M659.94,-215.7C662.1,-208.15 664.68,-199.12 667.09,-190.68\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"667.82,-199.59 668.11,-189 661.28,-197.1 667.82,-199.59\"/>\n",
"</g>\n",
"<!-- 4_0&#45;&gt;6_0 -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>4_0&#45;&gt;6_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M617.27,-218.33C597.6,-210.68 572.84,-201.05 549.52,-191.98\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"550.86,-188.36 540.28,-188 548.33,-194.88 550.86,-188.36\"/>\n",
"</g>\n",
"<!-- 4_1 -->\n",
"<g id=\"node16\" class=\"node\">\n",
"<title>4_1</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"495\" cy=\"-234\" rx=\"70.8\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"495\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____add__</text>\n",
"</g>\n",
"<!-- 4_1&#45;&gt;8_0 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>4_1&#45;&gt;8_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M532.73,-218.33C552.4,-210.68 577.16,-201.05 600.48,-191.98\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"601.67,-194.88 609.72,-188 599.14,-188.36 601.67,-194.88\"/>\n",
"</g>\n",
"<!-- 4_1&#45;&gt;6_0 -->\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>4_1&#45;&gt;6_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M490.06,-215.7C487.9,-208.15 485.32,-199.12 482.91,-190.68\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"488.72,-197.1 481.89,-189 482.18,-199.59 488.72,-197.1\"/>\n",
"</g>\n",
"<!-- 4_2 -->\n",
"<g id=\"node17\" class=\"node\">\n",
"<title>4_2</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"334\" cy=\"-234\" rx=\"72.34\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"334\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">Num____mul__</text>\n",
"</g>\n",
"<!-- 4_2&#45;&gt;3_0 -->\n",
"<g id=\"edge19\" class=\"edge\">\n",
"<title>4_2&#45;&gt;3_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M327.57,-215.7C324.74,-208.07 321.34,-198.92 318.18,-190.4\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"325.19,-194.84 316.35,-189 319.62,-199.08 325.19,-194.84\"/>\n",
"</g>\n",
"<!-- 4_2&#45;&gt;0_0 -->\n",
"<g id=\"edge18\" class=\"edge\">\n",
"<title>4_2&#45;&gt;0_0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M375.28,-218.85C387.91,-214.9 401.93,-210.91 415,-208 446.54,-200.99 535.87,-210.55 559,-188 576.92,-170.53 579.56,-141.24 578.55,-119.41\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"583.49,-125.88 577.71,-117 576.69,-127.55 583.49,-125.88\"/>\n",
"</g>\n",
"<!-- 4_3 -->\n",
"<g id=\"node18\" class=\"node\">\n",
"<title>4_3</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"212\" cy=\"-234\" rx=\"31.9\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"212\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">expr2</text>\n",
"</g>\n",
"<!-- 4_4 -->\n",
"<g id=\"node19\" class=\"node\">\n",
"<title>4_4</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"130\" cy=\"-234\" rx=\"31.9\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"130\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">expr2</text>\n",
"</g>\n",
"<!-- 4_5 -->\n",
"<g id=\"node20\" class=\"node\">\n",
"<title>4_5</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"48\" cy=\"-234\" rx=\"31.9\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"48\" y=\"-228.95\" font-family=\"Times,serif\" font-size=\"14.00\">expr1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"EGraph()"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a, b, c = vars_(\"a b c\", Num)\n",
"i, j = vars_(\"i j\", i64)\n",
"egraph.register(\n",
" rewrite(a + b).to(b + a),\n",
" rewrite(a * (b + c)).to((a * b) + (a * c)),\n",
" rewrite(Num(i) + Num(j)).to(Num(i + j)),\n",
" rewrite(Num(i) * Num(j)).to(Num(i * j)),\n",
")\n",
"egraph.run(10)\n",
"egraph.check(eq(expr1).to(expr2))\n",
"egraph"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "4f797f70-6dd4-47dc-be5d-5ef3ca6cb239",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.10.9"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Display the source blob
Display the rendered blob
Raw
graphviz-interacitve.ipynb
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment