eqsat-basic.ipynb

graphviz-interacitve.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "fe55c54f-8238-424f-9b30-1c7a34bbc798",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "from egglog import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "id": "8d253d3c-c720-4f5f-b7f6-7d71bb63ea3f",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "iterate(\"\"\"(function fib (i64) i64)\n",
    "(set (fib 0) 0)\n",
    "(set (fib 1) 1)\n",
    "\n",
    "(rule ((= f0 (fib x))\n",
    "       (= f1 (fib (+ x 1))))\n",
    "      ((set (fib (+ x 2)) (+ f0 f1))))\n",
    "\"\"\", 7)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "e083ec7f-6b97-4597-bf44-b66923108e13",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "iterate(\"\"\"(datatype Math\n",
    "  (Num i64)\n",
    "  (Var String)\n",
    "  (Add Math Math)\n",
    "  (Mul Math Math))\n",
    "\n",
    ";; expr1 = 2 * (x + 3)\n",
    "(define expr1 (Mul (Num 2) (Add (Var \"x\") (Num 3)))) \n",
    ";; expr2 = 6 + 2 * x\n",
    "(define expr2 (Add (Num 6) (Mul (Num 2) (Var \"x\"))))\n",
    "\n",
    "\n",
    ";; (rule ((= __root (Add a b)))\n",
    ";;       ((union __root (Add b a)))\n",
    "(rewrite (Add a b)\n",
    "         (Add b a))\n",
    "(rewrite (Mul a (Add b c))\n",
    "         (Add (Mul a b) (Mul a c)))\n",
    "(rewrite (Add (Num a) (Num b)) \n",
    "         (Num (+ a b)))\n",
    "(rewrite (Mul (Num a) (Num b))\n",
    "         (Num (* a b)))\n",
    "\"\"\", 10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "id": "33b5c154-045a-46e3-9143-03eeb544826d",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "iterate(\"\"\"(datatype Expr \n",
    "  (Num i64)\n",
    "  (Add Expr Expr))\n",
    "\n",
    "(function Fib (i64) Expr)\n",
    "\n",
    "(rewrite (Add (Num a) (Num b)) (Num (+ a b)))\n",
    "(rewrite (Fib x) (Add (Fib (- x 1)) (Fib (- x 2)))\n",
    "         :when ((> x 1)))\n",
    "(rewrite (Fib x) (Num x)\n",
    "         :when ((<= x 1)))\n",
    "\n",
    "(define f7 (Fib 7))\n",
    "\"\"\", 10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "id": "8b6959cb-9156-4f69-9dce-1f98840e22d9",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "iterate(\"\"\"(datatype expr \n",
    "    (Num i64)\n",
    "    (Add expr expr)\n",
    "    (Max expr expr))\n",
    "(rewrite (Add (Num a) (Num b)) (Num (+ a b)))\n",
    "(rewrite (Max (Num a) (Num b)) (Num (max a b)))\n",
    "\n",
    "; List of (weight, value) pairs\n",
    "(datatype objects\n",
    "    (Cons i64 i64 objects))\n",
    "(declare Nil objects)\n",
    "\n",
    "; Given a capacity and a list of objects, finds the maximum value of a\n",
    "; collection of objects whose total weight does not exceed the capacity.\n",
    "(function Knap (i64 objects) expr)\n",
    "\n",
    "(rule ((= f (Knap capacity (Cons weight val rest))) (<= weight capacity))\n",
    "      ((set (Knap capacity (Cons weight val rest))\n",
    "            (Max\n",
    "                (Add (Num val) (Knap (- capacity weight) rest))\n",
    "                (Knap capacity rest)))))\n",
    "\n",
    "(rule ((= f (Knap capacity (Cons weight val rest))) (> weight capacity))\n",
    "      ((set (Knap capacity (Cons weight val rest))\n",
    "            (Knap capacity rest))))\n",
    "\n",
    "(rule ((= f (Knap capacity Nil)))\n",
    "      ((set (Knap capacity Nil) (Num 0))))\n",
    "\n",
    "(define test1 (Knap 13 (Cons 5 5 (Cons 3 3 (Cons 12 12 (Cons 5 5 Nil))))))\n",
    "\n",
    "(define test2 (Knap 5 (Cons 6 6 Nil)))\n",
    "\n",
    "(define test3 (Knap 5 (Cons 1 1 (Cons 1 1 (Cons 1 1 Nil)))))\n",
    "\n",
    "(define test4 (Knap 15 (Cons 12 40 (Cons 2 20 (Cons 1 20 (Cons 1 10 (Cons 4 100 Nil)))))))\n",
    "\n",
    "\"\"\", 10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "7e9a9b13-f1bd-4fa5-aa23-5d74d7e213d3",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "def parse(s):\n",
    "    egraph = EGraph()\n",
    "    egraph._egraph.run_program(*egraph._egraph.parse_program(s))\n",
    "    return egraph"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "57962f75-51ce-430b-b261-9057fb83d1cc",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "from IPython.display import display, HTML\n",
    "import json\n",
    "from pathlib import Path"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "dbf1e565-771d-40ce-9cad-512aae931113",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "def iterate(s, i, run_str=\"(run 1)\"):\n",
    "    egraph = EGraph()\n",
    "    egraph._egraph.run_program(*egraph._egraph.parse_program(s))\n",
    "    dots = [egraph.graphviz()]\n",
    "    for _ in range(i):\n",
    "        egraph._egraph.run_program(*egraph._egraph.parse_program(run_str))\n",
    "        dots.append(egraph.graphviz())\n",
    "    html = MAGIC_STRING.replace(\"REPLACE_ME\", json.dumps(dots, indent=1))\n",
    "    Path(\"./index.html\").write_text(html)\n",
    "    # return HTML(html)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "75d4372b-981f-45ea-adf1-259f64895353",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "MAGIC_STRING = \"\"\"<!DOCTYPE html>\n",
    "<meta charset=\"utf-8\">\n",
    "<body>\n",
    "<script src=\"https://d3js.org/d3.v5.min.js\"></script>\n",
    "<script src=\"https://unpkg.com/[email protected]/viz.js\" type=\"javascript/worker\"></script>\n",
    "<script src=\"https://unpkg.com/[email protected]/build/d3-graphviz.min.js\"></script>\n",
    "<div id=\"graph\" style=\"text-align: center;\"></div>\n",
    "<script>\n",
    "\n",
    "var dotIndex = 0;\n",
    "var graphviz = d3.select(\"#graph\").graphviz()\n",
    "    .transition(function () {\n",
    "        return d3.transition(\"main\")\n",
    "            .ease(d3.easeLinear)\n",
    "            .delay(2000)\n",
    "            .duration(1800);\n",
    "    })\n",
    "    .logEvents(true)\n",
    "    .on(\"initEnd\", render);\n",
    "\n",
    "function render() {\n",
    "    var dot = dots[dotIndex];\n",
    "    graphviz\n",
    "        .renderDot(dot)\n",
    "        .on(\"end\", function () {\n",
    "            dotIndex = (dotIndex + 1) % dots.length;\n",
    "            render();\n",
    "        });\n",
    "}\n",
    "\n",
    "var dots = REPLACE_ME;\n",
    "\n",
    "</script>\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a4d81c8c-d9da-4af4-8e48-0cf3e1ea9a18",
   "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
}