.. DO NOT EDIT.
.. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY.
.. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE:
.. "auto_examples/eqsat_basic.py"
.. LINE NUMBERS ARE GIVEN BELOW.

.. only:: html

    .. note::
        :class: sphx-glr-download-link-note

        :ref:`Go to the end <sphx_glr_download_auto_examples_eqsat_basic.py>`
        to download the full example code

.. rst-class:: sphx-glr-example-title

.. _sphx_glr_auto_examples_eqsat_basic.py:


Basic equality saturation example.
==================================

.. GENERATED FROM PYTHON SOURCE LINES 5-44





.. raw:: html

    <div class="output_subarea output_html rendered_html output_result">
    <?xml version="1.0" encoding="UTF-8" standalone="no"?>
    <?xml-stylesheet href="/tmp/graphviz-styles.css" type="text/css"?>
    <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
     "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
    <!-- Generated by graphviz version 2.43.0 (0)
     -->
    <!-- Title: %3 Pages: 1 -->
    <svg width="349pt" height="309pt"
     viewBox="0.00 0.00 349.00 309.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
    <g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 305)">
    <title>%3</title>
    <polygon fill="white" stroke="#000000" points="-4,4 -4,-305 345,-305 345,4 -4,4"/>
    <g id="clust1" class="cluster">
    <title>outer_cluster_1</title>
    </g>
    <g id="clust2" class="cluster">
    <title>cluster_1</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M97,-90C97,-90 151,-90 151,-90 157,-90 163,-96 163,-102 163,-102 163,-120 163,-120 163,-126 157,-132 151,-132 151,-132 97,-132 97,-132 91,-132 85,-126 85,-120 85,-120 85,-102 85,-102 85,-96 91,-90 97,-90"/>
    </g>
    <g id="clust4" class="cluster">
    <title>outer_cluster_6</title>
    </g>
    <g id="clust5" class="cluster">
    <title>cluster_6</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M34,-169C34,-169 70,-169 70,-169 76,-169 82,-175 82,-181 82,-181 82,-199 82,-199 82,-205 76,-211 70,-211 70,-211 34,-211 34,-211 28,-211 22,-205 22,-199 22,-199 22,-181 22,-181 22,-175 28,-169 34,-169"/>
    </g>
    <g id="clust7" class="cluster">
    <title>outer_cluster_0</title>
    </g>
    <g id="clust8" class="cluster">
    <title>cluster_0</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M23,-90C23,-90 59,-90 59,-90 65,-90 71,-96 71,-102 71,-102 71,-120 71,-120 71,-126 65,-132 59,-132 59,-132 23,-132 23,-132 17,-132 11,-126 11,-120 11,-120 11,-102 11,-102 11,-96 17,-90 23,-90"/>
    </g>
    <g id="clust10" class="cluster">
    <title>outer_cluster_3</title>
    </g>
    <g id="clust11" class="cluster">
    <title>cluster_3</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M100,-169C100,-169 194,-169 194,-169 200,-169 206,-175 206,-181 206,-181 206,-199 206,-199 206,-205 200,-211 194,-211 194,-211 100,-211 100,-211 94,-211 88,-205 88,-199 88,-199 88,-181 88,-181 88,-175 94,-169 100,-169"/>
    </g>
    <g id="clust13" class="cluster">
    <title>outer_cluster_2</title>
    </g>
    <g id="clust14" class="cluster">
    <title>cluster_2</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M181,-90C181,-90 217,-90 217,-90 223,-90 229,-96 229,-102 229,-102 229,-120 229,-120 229,-126 223,-132 217,-132 217,-132 181,-132 181,-132 175,-132 169,-126 169,-120 169,-120 169,-102 169,-102 169,-96 175,-90 181,-90"/>
    </g>
    <g id="clust16" class="cluster">
    <title>outer_cluster_8</title>
    </g>
    <g id="clust17" class="cluster">
    <title>cluster_8</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M224,-169C224,-169 318,-169 318,-169 324,-169 330,-175 330,-181 330,-181 330,-199 330,-199 330,-205 324,-211 318,-211 318,-211 224,-211 224,-211 218,-211 212,-205 212,-199 212,-199 212,-181 212,-181 212,-175 218,-169 224,-169"/>
    </g>
    <g id="clust19" class="cluster">
    <title>outer_cluster_4</title>
    </g>
    <g id="clust20" class="cluster">
    <title>cluster_4</title>
    <path fill="#ffffb3" stroke="black" stroke-dasharray="5,2" d="M31,-248C31,-248 183,-248 183,-248 189,-248 195,-254 195,-260 195,-260 195,-278 195,-278 195,-284 189,-290 183,-290 183,-290 31,-290 31,-290 25,-290 19,-284 19,-278 19,-278 19,-260 19,-260 19,-254 25,-248 31,-248"/>
    </g>
    <g id="clust22" class="cluster">
    <title>outer_cluster_String&#45;1145338382888088809</title>
    </g>
    <g id="clust23" class="cluster">
    <title>cluster_String&#45;1145338382888088809</title>
    <path fill="#bebada" stroke="black" stroke-dasharray="5,2" d="M107,-11C107,-11 143,-11 143,-11 149,-11 155,-17 155,-23 155,-23 155,-41 155,-41 155,-47 149,-53 143,-53 143,-53 107,-53 107,-53 101,-53 95,-47 95,-41 95,-41 95,-23 95,-23 95,-17 101,-11 107,-11"/>
    </g>
    <g id="clust25" class="cluster">
    <title>outer_cluster_i64&#45;17615343019692007359</title>
    </g>
    <g id="clust26" class="cluster">
    <title>cluster_i64&#45;17615343019692007359</title>
    <path fill="#fb8072" stroke="black" stroke-dasharray="5,2" d="M181,-11C181,-11 217,-11 217,-11 223,-11 229,-17 229,-23 229,-23 229,-41 229,-41 229,-47 223,-53 217,-53 217,-53 181,-53 181,-53 175,-53 169,-47 169,-41 169,-41 169,-23 169,-23 169,-17 175,-11 181,-11"/>
    </g>
    <g id="clust28" class="cluster">
    <title>outer_cluster_i64&#45;11743562013128004906</title>
    </g>
    <g id="clust29" class="cluster">
    <title>cluster_i64&#45;11743562013128004906</title>
    <path fill="#fb8072" stroke="black" stroke-dasharray="5,2" d="M23,-11C23,-11 59,-11 59,-11 65,-11 71,-17 71,-23 71,-23 71,-41 71,-41 71,-47 65,-53 59,-53 59,-53 23,-53 23,-53 17,-53 11,-47 11,-41 11,-41 11,-23 11,-23 11,-17 17,-11 23,-11"/>
    </g>
    <g id="clust31" class="cluster">
    <title>outer_cluster_i64&#45;16783941965674463102</title>
    </g>
    <g id="clust32" class="cluster">
    <title>cluster_i64&#45;16783941965674463102</title>
    <path fill="#fb8072" stroke="black" stroke-dasharray="5,2" d="M282,-90C282,-90 318,-90 318,-90 324,-90 330,-96 330,-102 330,-102 330,-120 330,-120 330,-126 324,-132 318,-132 318,-132 282,-132 282,-132 276,-132 270,-126 270,-120 270,-120 270,-102 270,-102 270,-96 276,-90 282,-90"/>
    </g>
    <!-- Num_var&#45;1145338382888088809&#45;&gt;String&#45;1145338382888088809 -->
    <g id="edge1" class="edge">
    <title>Num_var&#45;1145338382888088809:s&#45;&gt;String&#45;1145338382888088809</title>
    <path fill="none" stroke="black" d="M125,-95C125,-81.84 125,-67.11 125,-55.3"/>
    <polygon fill="black" stroke="black" points="126.75,-58 125,-53 123.25,-58 126.75,-58"/>
    </g>
    <!-- Num___mul__&#45;5871781006564002453&#45;&gt;Num_var&#45;1145338382888088809 -->
    <g id="edge3" class="edge">
    <title>Num___mul__&#45;5871781006564002453:s&#45;&gt;Num_var&#45;1145338382888088809</title>
    <path fill="none" stroke="black" d="M63,-174C63,-156.76 75.14,-142.56 88.58,-132.12"/>
    <polygon fill="black" stroke="black" points="85.44,-136.11 88.79,-132 83.61,-133.13 85.44,-136.11"/>
    </g>
    <!-- Num___mul__&#45;5871781006564002453&#45;&gt;Num___init__&#45;11743562013128004906 -->
    <g id="edge2" class="edge">
    <title>Num___mul__&#45;5871781006564002453:s&#45;&gt;Num___init__&#45;11743562013128004906</title>
    <path fill="none" stroke="black" d="M41,-174C41,-160.84 41,-146.11 41,-134.3"/>
    <polygon fill="black" stroke="black" points="42.75,-137 41,-132 39.25,-137 42.75,-137"/>
    </g>
    <!-- Num___init__&#45;11743562013128004906&#45;&gt;i64&#45;11743562013128004906 -->
    <g id="edge4" class="edge">
    <title>Num___init__&#45;11743562013128004906:s&#45;&gt;i64&#45;11743562013128004906</title>
    <path fill="none" stroke="black" d="M41,-95C41,-81.84 41,-67.11 41,-55.3"/>
    <polygon fill="black" stroke="black" points="42.75,-58 41,-53 39.25,-58 42.75,-58"/>
    </g>
    <!-- Num___add__&#45;7659469028595837896&#45;&gt;Num_var&#45;1145338382888088809 -->
    <g id="edge5" class="edge">
    <title>Num___add__&#45;7659469028595837896:s&#45;&gt;Num_var&#45;1145338382888088809</title>
    <path fill="none" stroke="black" d="M164,-174C164,-158.71 155.31,-144.2 146.03,-133.07"/>
    <polygon fill="black" stroke="black" points="149.65,-133.6 144.59,-132 147.55,-136.4 149.65,-133.6"/>
    </g>
    <!-- Num___add__&#45;7659469028595837896&#45;&gt;Num___init__&#45;17615343019692007359 -->
    <g id="edge6" class="edge">
    <title>Num___add__&#45;7659469028595837896:s&#45;&gt;Num___init__&#45;17615343019692007359</title>
    <path fill="none" stroke="black" d="M189,-174C189,-160.76 191.25,-146.14 193.61,-134.42"/>
    <polygon fill="black" stroke="black" points="194.25,-137.28 194.7,-132 191.05,-135.84 194.25,-137.28"/>
    </g>
    <!-- Num___init__&#45;17615343019692007359&#45;&gt;i64&#45;17615343019692007359 -->
    <g id="edge9" class="edge">
    <title>Num___init__&#45;17615343019692007359:s&#45;&gt;i64&#45;17615343019692007359</title>
    <path fill="none" stroke="black" d="M199,-95C199,-81.84 199,-67.11 199,-55.3"/>
    <polygon fill="black" stroke="black" points="200.75,-58 199,-53 197.25,-58 200.75,-58"/>
    </g>
    <!-- Num___add__&#45;7784354942592584825&#45;&gt;Num_var&#45;1145338382888088809 -->
    <g id="edge8" class="edge">
    <title>Num___add__&#45;7784354942592584825:s&#45;&gt;Num_var&#45;1145338382888088809</title>
    <path fill="none" stroke="black" d="M131,-174C131,-160.76 129.4,-146.02 127.73,-134.24"/>
    <polygon fill="black" stroke="black" points="130.24,-136.16 126.97,-132 126.93,-137.3 130.24,-136.16"/>
    </g>
    <!-- Num___add__&#45;7784354942592584825&#45;&gt;Num___init__&#45;17615343019692007359 -->
    <g id="edge7" class="edge">
    <title>Num___add__&#45;7784354942592584825:s&#45;&gt;Num___init__&#45;17615343019692007359</title>
    <path fill="none" stroke="black" d="M106,-174C106,-173.52 141.66,-149.86 168.82,-131.91"/>
    <polygon fill="black" stroke="black" points="169.62,-136.35 169,-131.09 166.2,-135.59 169.62,-136.35"/>
    </g>
    <!-- Num___init__&#45;16783941965674463102&#45;&gt;i64&#45;16783941965674463102 -->
    <g id="edge10" class="edge">
    <title>Num___init__&#45;16783941965674463102:s&#45;&gt;i64&#45;16783941965674463102</title>
    <path fill="none" stroke="black" d="M300,-174C300,-160.84 300,-146.11 300,-134.3"/>
    <polygon fill="black" stroke="black" points="301.75,-137 300,-132 298.25,-137 301.75,-137"/>
    </g>
    <!-- Num___mul__&#45;11743562013128004906&#45;&gt;Num___init__&#45;11743562013128004906 -->
    <g id="edge11" class="edge">
    <title>Num___mul__&#45;11743562013128004906:s&#45;&gt;Num___init__&#45;11743562013128004906</title>
    <path fill="none" stroke="black" d="M231,-174C231,-162.76 217.79,-169.15 207,-166 152.89,-150.19 136.58,-155.34 84,-135 80.42,-133.61 76.75,-132 73.15,-130.27"/>
    <polygon fill="black" stroke="black" points="76.14,-130.14 71,-128.87 74.23,-133.07 76.14,-130.14"/>
    </g>
    <!-- Num___mul__&#45;11743562013128004906&#45;&gt;Num___init__&#45;17615343019692007359 -->
    <g id="edge12" class="edge">
    <title>Num___mul__&#45;11743562013128004906:s&#45;&gt;Num___init__&#45;17615343019692007359</title>
    <path fill="none" stroke="black" d="M253,-174C253,-157.46 241.93,-143.18 229.82,-132.52"/>
    <polygon fill="black" stroke="black" points="232.95,-134.57 229,-131.04 229.89,-136.26 232.95,-134.57"/>
    </g>
    <!-- Num___mul__&#45;17615343019692007359&#45;&gt;Num___init__&#45;11743562013128004906 -->
    <g id="edge13" class="edge">
    <title>Num___mul__&#45;17615343019692007359:s&#45;&gt;Num___init__&#45;11743562013128004906</title>
    <path fill="none" stroke="black" d="M38,-253C38,-234.09 24.86,-232.51 21,-214 16.65,-193.12 17.24,-187 21,-166 22.95,-155.11 26.96,-143.54 30.87,-133.91"/>
    <polygon fill="black" stroke="black" points="31.07,-137.23 31.9,-132 27.99,-135.57 31.07,-137.23"/>
    </g>
    <!-- Num___mul__&#45;17615343019692007359&#45;&gt;Num___add__&#45;7784354942592584825 -->
    <g id="edge14" class="edge">
    <title>Num___mul__&#45;17615343019692007359:s&#45;&gt;Num___add__&#45;7784354942592584825</title>
    <path fill="none" stroke="black" d="M60,-253C60,-242.74 77.15,-225.31 92.8,-211.53"/>
    <polygon fill="black" stroke="black" points="90.26,-215 93.73,-211 88.52,-211.96 90.26,-215"/>
    </g>
    <!-- Num___add__&#45;16545935510313822457&#45;&gt;Num___mul__&#45;5871781006564002453 -->
    <g id="edge15" class="edge">
    <title>Num___add__&#45;16545935510313822457:s&#45;&gt;Num___mul__&#45;5871781006564002453</title>
    <path fill="none" stroke="black" d="M95,-253C95,-237.48 85.79,-223.05 75.9,-212.02"/>
    <polygon fill="black" stroke="black" points="79.42,-212.14 74.24,-211 77.58,-215.11 79.42,-212.14"/>
    </g>
    <!-- Num___add__&#45;16545935510313822457&#45;&gt;Num___mul__&#45;11743562013128004906 -->
    <g id="edge16" class="edge">
    <title>Num___add__&#45;16545935510313822457:s&#45;&gt;Num___mul__&#45;11743562013128004906</title>
    <path fill="none" stroke="black" d="M120,-253C120,-210.63 169.84,-234.37 207,-214 207.22,-213.88 207.43,-213.76 207.65,-213.64"/>
    <polygon fill="black" stroke="black" points="208.79,-215.01 212.26,-211 207.05,-211.97 208.79,-215.01"/>
    </g>
    <!-- Num___add__&#45;5000171696738118755&#45;&gt;Num___mul__&#45;5871781006564002453 -->
    <g id="edge18" class="edge">
    <title>Num___add__&#45;5000171696738118755:s&#45;&gt;Num___mul__&#45;5871781006564002453</title>
    <path fill="none" stroke="black" d="M178,-253C178,-209 125.76,-234.83 87,-214 86.78,-213.88 86.56,-213.76 86.34,-213.64"/>
    <polygon fill="black" stroke="black" points="86.88,-211.94 81.66,-211 85.15,-214.98 86.88,-211.94"/>
    </g>
    <!-- Num___add__&#45;5000171696738118755&#45;&gt;Num___init__&#45;16783941965674463102 -->
    <g id="edge17" class="edge">
    <title>Num___add__&#45;5000171696738118755:s&#45;&gt;Num___init__&#45;16783941965674463102</title>
    <path fill="none" stroke="black" d="M153,-253C153,-198.61 220.79,-239.18 269,-214 270.7,-213.11 272.42,-212.13 274.11,-211.09"/>
    <polygon fill="black" stroke="black" points="270.02,-213.76 274.55,-211 269.29,-210.33 270.02,-213.76"/>
    </g>
    <!-- Num_var&#45;1145338382888088809 -->
    <g id="node1" class="node">
    <title>Num_var&#45;1145338382888088809</title>
    <g id="a_node1"><a xlink:title="1: Num_var&#45;1145338382888088809">
    <path fill="white" stroke="transparent" d="M99.17,-95C99.17,-95 148.83,-95 148.83,-95 154.17,-95 159.5,-100.33 159.5,-105.67 159.5,-105.67 159.5,-116.33 159.5,-116.33 159.5,-121.67 154.17,-127 148.83,-127 148.83,-127 99.17,-127 99.17,-127 93.83,-127 88.5,-121.67 88.5,-116.33 88.5,-116.33 88.5,-105.67 88.5,-105.67 88.5,-100.33 93.83,-95 99.17,-95"/>
    <text text-anchor="start" x="94" y="-107.3" font-family="Helvetica,sans-Serif" font-size="14.00">Num.var</text>
    <path fill="none" stroke="black" d="M99.17,-95C99.17,-95 148.83,-95 148.83,-95 154.17,-95 159.5,-100.33 159.5,-105.67 159.5,-105.67 159.5,-116.33 159.5,-116.33 159.5,-121.67 154.17,-127 148.83,-127 148.83,-127 99.17,-127 99.17,-127 93.83,-127 88.5,-121.67 88.5,-116.33 88.5,-116.33 88.5,-105.67 88.5,-105.67 88.5,-100.33 93.83,-95 99.17,-95"/>
    </a>
    </g>
    </g>
    <!-- String&#45;1145338382888088809 -->
    <g id="node2" class="node">
    <title>String&#45;1145338382888088809</title>
    <g id="a_node2"><a xlink:title="String&#45;1145338382888088809: String&#45;1145338382888088809">
    <path fill="white" stroke="transparent" d="M119.67,-16C119.67,-16 130.33,-16 130.33,-16 135.67,-16 141,-21.33 141,-26.67 141,-26.67 141,-37.33 141,-37.33 141,-42.67 135.67,-48 130.33,-48 130.33,-48 119.67,-48 119.67,-48 114.33,-48 109,-42.67 109,-37.33 109,-37.33 109,-26.67 109,-26.67 109,-21.33 114.33,-16 119.67,-16"/>
    <text text-anchor="start" x="114" y="-28.3" font-family="Helvetica,sans-Serif" font-size="14.00">&quot;x&quot;</text>
    <path fill="none" stroke="black" d="M119.67,-16C119.67,-16 130.33,-16 130.33,-16 135.67,-16 141,-21.33 141,-26.67 141,-26.67 141,-37.33 141,-37.33 141,-42.67 135.67,-48 130.33,-48 130.33,-48 119.67,-48 119.67,-48 114.33,-48 109,-42.67 109,-37.33 109,-37.33 109,-26.67 109,-26.67 109,-21.33 114.33,-16 119.67,-16"/>
    </a>
    </g>
    </g>
    <!-- Num___mul__&#45;5871781006564002453 -->
    <g id="node3" class="node">
    <title>Num___mul__&#45;5871781006564002453</title>
    <g id="a_node3"><a xlink:title="6: Num___mul__&#45;5871781006564002453">
    <path fill="white" stroke="transparent" d="M39.67,-174C39.67,-174 64.33,-174 64.33,-174 69.67,-174 75,-179.33 75,-184.67 75,-184.67 75,-195.33 75,-195.33 75,-200.67 69.67,-206 64.33,-206 64.33,-206 39.67,-206 39.67,-206 34.33,-206 29,-200.67 29,-195.33 29,-195.33 29,-184.67 29,-184.67 29,-179.33 34.33,-174 39.67,-174"/>
    <text text-anchor="start" x="34" y="-186.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· * ·)</text>
    <path fill="none" stroke="black" d="M39.67,-174C39.67,-174 64.33,-174 64.33,-174 69.67,-174 75,-179.33 75,-184.67 75,-184.67 75,-195.33 75,-195.33 75,-200.67 69.67,-206 64.33,-206 64.33,-206 39.67,-206 39.67,-206 34.33,-206 29,-200.67 29,-195.33 29,-195.33 29,-184.67 29,-184.67 29,-179.33 34.33,-174 39.67,-174"/>
    </a>
    </g>
    </g>
    <!-- Num___init__&#45;11743562013128004906 -->
    <g id="node4" class="node">
    <title>Num___init__&#45;11743562013128004906</title>
    <g id="a_node4"><a xlink:title="0: Num___init__&#45;11743562013128004906">
    <path fill="white" stroke="transparent" d="M29.67,-95C29.67,-95 52.33,-95 52.33,-95 57.67,-95 63,-100.33 63,-105.67 63,-105.67 63,-116.33 63,-116.33 63,-121.67 57.67,-127 52.33,-127 52.33,-127 29.67,-127 29.67,-127 24.33,-127 19,-121.67 19,-116.33 19,-116.33 19,-105.67 19,-105.67 19,-100.33 24.33,-95 29.67,-95"/>
    <text text-anchor="start" x="24" y="-107.3" font-family="Helvetica,sans-Serif" font-size="14.00">Num</text>
    <path fill="none" stroke="black" d="M29.67,-95C29.67,-95 52.33,-95 52.33,-95 57.67,-95 63,-100.33 63,-105.67 63,-105.67 63,-116.33 63,-116.33 63,-121.67 57.67,-127 52.33,-127 52.33,-127 29.67,-127 29.67,-127 24.33,-127 19,-121.67 19,-116.33 19,-116.33 19,-105.67 19,-105.67 19,-100.33 24.33,-95 29.67,-95"/>
    </a>
    </g>
    </g>
    <!-- i64&#45;11743562013128004906 -->
    <g id="node5" class="node">
    <title>i64&#45;11743562013128004906</title>
    <g id="a_node5"><a xlink:title="i64&#45;11743562013128004906: i64&#45;11743562013128004906">
    <path fill="white" stroke="transparent" d="M35.67,-16C35.67,-16 46.33,-16 46.33,-16 51.67,-16 57,-21.33 57,-26.67 57,-26.67 57,-37.33 57,-37.33 57,-42.67 51.67,-48 46.33,-48 46.33,-48 35.67,-48 35.67,-48 30.33,-48 25,-42.67 25,-37.33 25,-37.33 25,-26.67 25,-26.67 25,-21.33 30.33,-16 35.67,-16"/>
    <text text-anchor="start" x="36" y="-28.3" font-family="Helvetica,sans-Serif" font-size="14.00">2</text>
    <path fill="none" stroke="black" d="M35.67,-16C35.67,-16 46.33,-16 46.33,-16 51.67,-16 57,-21.33 57,-26.67 57,-26.67 57,-37.33 57,-37.33 57,-42.67 51.67,-48 46.33,-48 46.33,-48 35.67,-48 35.67,-48 30.33,-48 25,-42.67 25,-37.33 25,-37.33 25,-26.67 25,-26.67 25,-21.33 30.33,-16 35.67,-16"/>
    </a>
    </g>
    </g>
    <!-- Num___add__&#45;7659469028595837896 -->
    <g id="node6" class="node">
    <title>Num___add__&#45;7659469028595837896</title>
    <g id="a_node6"><a xlink:title="3: Num___add__&#45;7659469028595837896">
    <path fill="white" stroke="transparent" d="M161.17,-174C161.17,-174 190.83,-174 190.83,-174 196.17,-174 201.5,-179.33 201.5,-184.67 201.5,-184.67 201.5,-195.33 201.5,-195.33 201.5,-200.67 196.17,-206 190.83,-206 190.83,-206 161.17,-206 161.17,-206 155.83,-206 150.5,-200.67 150.5,-195.33 150.5,-195.33 150.5,-184.67 150.5,-184.67 150.5,-179.33 155.83,-174 161.17,-174"/>
    <text text-anchor="start" x="156" y="-186.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· + ·)</text>
    <path fill="none" stroke="black" d="M161.17,-174C161.17,-174 190.83,-174 190.83,-174 196.17,-174 201.5,-179.33 201.5,-184.67 201.5,-184.67 201.5,-195.33 201.5,-195.33 201.5,-200.67 196.17,-206 190.83,-206 190.83,-206 161.17,-206 161.17,-206 155.83,-206 150.5,-200.67 150.5,-195.33 150.5,-195.33 150.5,-184.67 150.5,-184.67 150.5,-179.33 155.83,-174 161.17,-174"/>
    </a>
    </g>
    </g>
    <!-- Num___init__&#45;17615343019692007359 -->
    <g id="node7" class="node">
    <title>Num___init__&#45;17615343019692007359</title>
    <g id="a_node7"><a xlink:title="2: Num___init__&#45;17615343019692007359">
    <path fill="white" stroke="transparent" d="M187.67,-95C187.67,-95 210.33,-95 210.33,-95 215.67,-95 221,-100.33 221,-105.67 221,-105.67 221,-116.33 221,-116.33 221,-121.67 215.67,-127 210.33,-127 210.33,-127 187.67,-127 187.67,-127 182.33,-127 177,-121.67 177,-116.33 177,-116.33 177,-105.67 177,-105.67 177,-100.33 182.33,-95 187.67,-95"/>
    <text text-anchor="start" x="182" y="-107.3" font-family="Helvetica,sans-Serif" font-size="14.00">Num</text>
    <path fill="none" stroke="black" d="M187.67,-95C187.67,-95 210.33,-95 210.33,-95 215.67,-95 221,-100.33 221,-105.67 221,-105.67 221,-116.33 221,-116.33 221,-121.67 215.67,-127 210.33,-127 210.33,-127 187.67,-127 187.67,-127 182.33,-127 177,-121.67 177,-116.33 177,-116.33 177,-105.67 177,-105.67 177,-100.33 182.33,-95 187.67,-95"/>
    </a>
    </g>
    </g>
    <!-- Num___add__&#45;7784354942592584825 -->
    <g id="node8" class="node">
    <title>Num___add__&#45;7784354942592584825</title>
    <g id="a_node8"><a xlink:title="3: Num___add__&#45;7784354942592584825">
    <path fill="white" stroke="transparent" d="M103.17,-174C103.17,-174 132.83,-174 132.83,-174 138.17,-174 143.5,-179.33 143.5,-184.67 143.5,-184.67 143.5,-195.33 143.5,-195.33 143.5,-200.67 138.17,-206 132.83,-206 132.83,-206 103.17,-206 103.17,-206 97.83,-206 92.5,-200.67 92.5,-195.33 92.5,-195.33 92.5,-184.67 92.5,-184.67 92.5,-179.33 97.83,-174 103.17,-174"/>
    <text text-anchor="start" x="98" y="-186.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· + ·)</text>
    <path fill="none" stroke="black" d="M103.17,-174C103.17,-174 132.83,-174 132.83,-174 138.17,-174 143.5,-179.33 143.5,-184.67 143.5,-184.67 143.5,-195.33 143.5,-195.33 143.5,-200.67 138.17,-206 132.83,-206 132.83,-206 103.17,-206 103.17,-206 97.83,-206 92.5,-200.67 92.5,-195.33 92.5,-195.33 92.5,-184.67 92.5,-184.67 92.5,-179.33 97.83,-174 103.17,-174"/>
    </a>
    </g>
    </g>
    <!-- i64&#45;17615343019692007359 -->
    <g id="node9" class="node">
    <title>i64&#45;17615343019692007359</title>
    <g id="a_node9"><a xlink:title="i64&#45;17615343019692007359: i64&#45;17615343019692007359">
    <path fill="white" stroke="transparent" d="M193.67,-16C193.67,-16 204.33,-16 204.33,-16 209.67,-16 215,-21.33 215,-26.67 215,-26.67 215,-37.33 215,-37.33 215,-42.67 209.67,-48 204.33,-48 204.33,-48 193.67,-48 193.67,-48 188.33,-48 183,-42.67 183,-37.33 183,-37.33 183,-26.67 183,-26.67 183,-21.33 188.33,-16 193.67,-16"/>
    <text text-anchor="start" x="194" y="-28.3" font-family="Helvetica,sans-Serif" font-size="14.00">3</text>
    <path fill="none" stroke="black" d="M193.67,-16C193.67,-16 204.33,-16 204.33,-16 209.67,-16 215,-21.33 215,-26.67 215,-26.67 215,-37.33 215,-37.33 215,-42.67 209.67,-48 204.33,-48 204.33,-48 193.67,-48 193.67,-48 188.33,-48 183,-42.67 183,-37.33 183,-37.33 183,-26.67 183,-26.67 183,-21.33 188.33,-16 193.67,-16"/>
    </a>
    </g>
    </g>
    <!-- Num___init__&#45;16783941965674463102 -->
    <g id="node10" class="node">
    <title>Num___init__&#45;16783941965674463102</title>
    <g id="a_node10"><a xlink:title="8: Num___init__&#45;16783941965674463102">
    <path fill="white" stroke="transparent" d="M288.67,-174C288.67,-174 311.33,-174 311.33,-174 316.67,-174 322,-179.33 322,-184.67 322,-184.67 322,-195.33 322,-195.33 322,-200.67 316.67,-206 311.33,-206 311.33,-206 288.67,-206 288.67,-206 283.33,-206 278,-200.67 278,-195.33 278,-195.33 278,-184.67 278,-184.67 278,-179.33 283.33,-174 288.67,-174"/>
    <text text-anchor="start" x="283" y="-186.3" font-family="Helvetica,sans-Serif" font-size="14.00">Num</text>
    <path fill="none" stroke="black" d="M288.67,-174C288.67,-174 311.33,-174 311.33,-174 316.67,-174 322,-179.33 322,-184.67 322,-184.67 322,-195.33 322,-195.33 322,-200.67 316.67,-206 311.33,-206 311.33,-206 288.67,-206 288.67,-206 283.33,-206 278,-200.67 278,-195.33 278,-195.33 278,-184.67 278,-184.67 278,-179.33 283.33,-174 288.67,-174"/>
    </a>
    </g>
    </g>
    <!-- i64&#45;16783941965674463102 -->
    <g id="node11" class="node">
    <title>i64&#45;16783941965674463102</title>
    <g id="a_node11"><a xlink:title="i64&#45;16783941965674463102: i64&#45;16783941965674463102">
    <path fill="white" stroke="transparent" d="M294.67,-95C294.67,-95 305.33,-95 305.33,-95 310.67,-95 316,-100.33 316,-105.67 316,-105.67 316,-116.33 316,-116.33 316,-121.67 310.67,-127 305.33,-127 305.33,-127 294.67,-127 294.67,-127 289.33,-127 284,-121.67 284,-116.33 284,-116.33 284,-105.67 284,-105.67 284,-100.33 289.33,-95 294.67,-95"/>
    <text text-anchor="start" x="295" y="-107.3" font-family="Helvetica,sans-Serif" font-size="14.00">6</text>
    <path fill="none" stroke="black" d="M294.67,-95C294.67,-95 305.33,-95 305.33,-95 310.67,-95 316,-100.33 316,-105.67 316,-105.67 316,-116.33 316,-116.33 316,-121.67 310.67,-127 305.33,-127 305.33,-127 294.67,-127 294.67,-127 289.33,-127 284,-121.67 284,-116.33 284,-116.33 284,-105.67 284,-105.67 284,-100.33 289.33,-95 294.67,-95"/>
    </a>
    </g>
    </g>
    <!-- Num___mul__&#45;11743562013128004906 -->
    <g id="node12" class="node">
    <title>Num___mul__&#45;11743562013128004906</title>
    <g id="a_node12"><a xlink:title="8: Num___mul__&#45;11743562013128004906">
    <path fill="white" stroke="transparent" d="M229.67,-174C229.67,-174 254.33,-174 254.33,-174 259.67,-174 265,-179.33 265,-184.67 265,-184.67 265,-195.33 265,-195.33 265,-200.67 259.67,-206 254.33,-206 254.33,-206 229.67,-206 229.67,-206 224.33,-206 219,-200.67 219,-195.33 219,-195.33 219,-184.67 219,-184.67 219,-179.33 224.33,-174 229.67,-174"/>
    <text text-anchor="start" x="224" y="-186.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· * ·)</text>
    <path fill="none" stroke="black" d="M229.67,-174C229.67,-174 254.33,-174 254.33,-174 259.67,-174 265,-179.33 265,-184.67 265,-184.67 265,-195.33 265,-195.33 265,-200.67 259.67,-206 254.33,-206 254.33,-206 229.67,-206 229.67,-206 224.33,-206 219,-200.67 219,-195.33 219,-195.33 219,-184.67 219,-184.67 219,-179.33 224.33,-174 229.67,-174"/>
    </a>
    </g>
    </g>
    <!-- Num___mul__&#45;17615343019692007359 -->
    <g id="node13" class="node">
    <title>Num___mul__&#45;17615343019692007359</title>
    <g id="a_node13"><a xlink:title="4: Num___mul__&#45;17615343019692007359">
    <path fill="white" stroke="transparent" d="M36.67,-253C36.67,-253 61.33,-253 61.33,-253 66.67,-253 72,-258.33 72,-263.67 72,-263.67 72,-274.33 72,-274.33 72,-279.67 66.67,-285 61.33,-285 61.33,-285 36.67,-285 36.67,-285 31.33,-285 26,-279.67 26,-274.33 26,-274.33 26,-263.67 26,-263.67 26,-258.33 31.33,-253 36.67,-253"/>
    <text text-anchor="start" x="31" y="-265.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· * ·)</text>
    <path fill="none" stroke="black" d="M36.67,-253C36.67,-253 61.33,-253 61.33,-253 66.67,-253 72,-258.33 72,-263.67 72,-263.67 72,-274.33 72,-274.33 72,-279.67 66.67,-285 61.33,-285 61.33,-285 36.67,-285 36.67,-285 31.33,-285 26,-279.67 26,-274.33 26,-274.33 26,-263.67 26,-263.67 26,-258.33 31.33,-253 36.67,-253"/>
    </a>
    </g>
    </g>
    <!-- Num___add__&#45;16545935510313822457 -->
    <g id="node14" class="node">
    <title>Num___add__&#45;16545935510313822457</title>
    <g id="a_node14"><a xlink:title="4: Num___add__&#45;16545935510313822457">
    <path fill="white" stroke="transparent" d="M92.17,-253C92.17,-253 121.83,-253 121.83,-253 127.17,-253 132.5,-258.33 132.5,-263.67 132.5,-263.67 132.5,-274.33 132.5,-274.33 132.5,-279.67 127.17,-285 121.83,-285 121.83,-285 92.17,-285 92.17,-285 86.83,-285 81.5,-279.67 81.5,-274.33 81.5,-274.33 81.5,-263.67 81.5,-263.67 81.5,-258.33 86.83,-253 92.17,-253"/>
    <text text-anchor="start" x="87" y="-265.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· + ·)</text>
    <path fill="none" stroke="black" d="M92.17,-253C92.17,-253 121.83,-253 121.83,-253 127.17,-253 132.5,-258.33 132.5,-263.67 132.5,-263.67 132.5,-274.33 132.5,-274.33 132.5,-279.67 127.17,-285 121.83,-285 121.83,-285 92.17,-285 92.17,-285 86.83,-285 81.5,-279.67 81.5,-274.33 81.5,-274.33 81.5,-263.67 81.5,-263.67 81.5,-258.33 86.83,-253 92.17,-253"/>
    </a>
    </g>
    </g>
    <!-- Num___add__&#45;5000171696738118755 -->
    <g id="node15" class="node">
    <title>Num___add__&#45;5000171696738118755</title>
    <g id="a_node15"><a xlink:title="4: Num___add__&#45;5000171696738118755">
    <path fill="white" stroke="transparent" d="M150.17,-253C150.17,-253 179.83,-253 179.83,-253 185.17,-253 190.5,-258.33 190.5,-263.67 190.5,-263.67 190.5,-274.33 190.5,-274.33 190.5,-279.67 185.17,-285 179.83,-285 179.83,-285 150.17,-285 150.17,-285 144.83,-285 139.5,-279.67 139.5,-274.33 139.5,-274.33 139.5,-263.67 139.5,-263.67 139.5,-258.33 144.83,-253 150.17,-253"/>
    <text text-anchor="start" x="145" y="-265.3" font-family="Helvetica,sans-Serif" font-size="14.00">(· + ·)</text>
    <path fill="none" stroke="black" d="M150.17,-253C150.17,-253 179.83,-253 179.83,-253 185.17,-253 190.5,-258.33 190.5,-263.67 190.5,-263.67 190.5,-274.33 190.5,-274.33 190.5,-279.67 185.17,-285 179.83,-285 179.83,-285 150.17,-285 150.17,-285 144.83,-285 139.5,-279.67 139.5,-274.33 139.5,-274.33 139.5,-263.67 139.5,-263.67 139.5,-258.33 144.83,-253 150.17,-253"/>
    </a>
    </g>
    </g>
    </g>
    </svg>

    </div>
    <br />
    <br />

.. code-block:: Python

    from __future__ import annotations

    from egglog import *

    egraph = EGraph()


    @egraph.class_
    class Num(Expr):
        def __init__(self, value: i64Like) -> None:
            ...

        @classmethod
        def var(cls, name: StringLike) -> Num:  # type: ignore[empty-body]
            ...

        def __add__(self, other: Num) -> Num:  # type: ignore[empty-body]
            ...

        def __mul__(self, other: Num) -> Num:  # type: ignore[empty-body]
            ...


    # expr1 = 2 * (x + 3)
    expr1 = egraph.let("expr1", Num(2) * (Num.var("x") + Num(3)))
    # expr2 = 6 + 2 * x
    expr2 = egraph.let("expr2", Num(6) + Num(2) * Num.var("x"))

    a, b, c = vars_("a b c", Num)
    i, j = vars_("i j", i64)
    egraph.register(
        rewrite(a + b).to(b + a),
        rewrite(a * (b + c)).to((a * b) + (a * c)),
        rewrite(Num(i) + Num(j)).to(Num(i + j)),
        rewrite(Num(i) * Num(j)).to(Num(i * j)),
    )
    egraph.run(10)
    egraph.check(eq(expr1).to(expr2))
    egraph


.. rst-class:: sphx-glr-timing

   **Total running time of the script:** (0 minutes 0.047 seconds)


.. _sphx_glr_download_auto_examples_eqsat_basic.py:

.. only:: html

  .. container:: sphx-glr-footer sphx-glr-footer-example

    .. container:: sphx-glr-download sphx-glr-download-jupyter

      :download:`Download Jupyter notebook: eqsat_basic.ipynb <eqsat_basic.ipynb>`

    .. container:: sphx-glr-download sphx-glr-download-python

      :download:`Download Python source code: eqsat_basic.py <eqsat_basic.py>`


.. only:: html

 .. rst-class:: sphx-glr-signature

    `Gallery generated by Sphinx-Gallery <https://sphinx-gallery.github.io>`_