# mypy: disable-error-code="empty-body"
"""
Basic equality saturation example.
==================================
"""

'\nBasic equality saturation example.\n==================================\n'

from __future__ import annotations

from egglog import *

egraph = EGraph()

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

    @classmethod
    def var(cls, name: StringLike) -> Num: ...

    def __add__(self, other: Num) -> Num: ...

    def __mul__(self, other: Num) -> Num: ...

expr1 = Num(2) * (Num.var("x") + Num(3))
expr2 = Num(6) + Num(2) * Num.var("x")

a, b, c = vars_("a b c", Num)
i, j = vars_("i j", i64)

egraph = EGraph()
egraph.register(expr1, expr2)

egraph.run(
    ruleset(
        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)),
    )
    * 10
)

RunReport(iterations=[IterationReport(rule_set_report=RuleSetReport(changed=True, rule_reports={'rewrite(a + b).to(b + a)': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=2)], 'rewrite(a * (b + c)).to(a * b + a * c)': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=1)], 'rewrite(Num(i) + Num(j)).to(Num(i + j))': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0)], 'rewrite(Num(i) * Num(j)).to(Num(i * j))': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0)]}, search_and_apply_time=0:00:00, merge_time=0:00:00), rebuild_time=datetime.timedelta(0)), IterationReport(rule_set_report=RuleSetReport(changed=True, rule_reports={'rewrite(a + b).to(b + a)': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=3)], 'rewrite(a * (b + c)).to(a * b + a * c)': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=1), RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0)], 'rewrite(Num(i) + Num(j)).to(Num(i + j))': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0)], 'rewrite(Num(i) * Num(j)).to(Num(i * j))': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=1)]}, search_and_apply_time=0:00:00, merge_time=0:00:00), rebuild_time=datetime.timedelta(0)), IterationReport(rule_set_report=RuleSetReport(changed=False, rule_reports={'rewrite(Num(i) * Num(j)).to(Num(i * j))': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=1)], 'rewrite(Num(i) + Num(j)).to(Num(i + j))': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0)], 'rewrite(a + b).to(b + a)': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=2)], 'rewrite(a * (b + c)).to(a * b + a * c)': [RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0), RuleReport(plan=None, search_and_apply_time=datetime.timedelta(0), num_matches=0)]}, search_and_apply_time=0:00:00, merge_time=0:00:00), rebuild_time=datetime.timedelta(0))], updated=True, search_and_apply_time_per_rule={'rewrite(Num(i) + Num(j)).to(Num(i + j))': datetime.timedelta(0), 'rewrite(Num(i) * Num(j)).to(Num(i * j))': datetime.timedelta(0), 'rewrite(a * (b + c)).to(a * b + a * c)': datetime.timedelta(0), 'rewrite(a + b).to(b + a)': datetime.timedelta(0)}, num_matches_per_rule={'rewrite(a + b).to(b + a)': 7, 'rewrite(a * (b + c)).to(a * b + a * c)': 2, 'rewrite(Num(i) + Num(j)).to(Num(i + j))': 0, 'rewrite(Num(i) * Num(j)).to(Num(i * j))': 2}, search_and_apply_time_per_ruleset={'ruleset_125708326480128': datetime.timedelta(0)}, merge_time_per_ruleset={'ruleset_125708326480128': datetime.timedelta(0)}, rebuild_time_per_ruleset={'ruleset_125708326480128': datetime.timedelta(0)})

egraph.check(expr1 == expr2)