%3

.. DO NOT EDIT. .. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY. .. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE: .. "auto_examples/resolution.py" .. LINE NUMBERS ARE GIVEN BELOW. .. only:: html .. note:: :class: sphx-glr-download-link-note :ref:`Go to the end ` to download the full example code. .. rst-class:: sphx-glr-example-title .. _sphx_glr_auto_examples_resolution.py: Resolution theorem proving. =========================== .. GENERATED FROM PYTHON SOURCE LINES 5-85 .. raw:: html

.. code-block:: Python from __future__ import annotations from typing import ClassVar from egglog import * egraph = EGraph() class Boolean(Expr): FALSE: ClassVar[Boolean] def __or__(self, other: Boolean) -> Boolean: # type: ignore[empty-body] ... def __invert__(self) -> Boolean: # type: ignore[empty-body] ... # Show off two ways of creating constants, either as top level values or as classvars T = constant("T", Boolean) F = Boolean.FALSE p, a, b, c, as_, bs = vars_("p a b c as bs", Boolean) egraph.register( # clauses are assumed in the normal form (or a (or b (or c False))) union(~F).with_(T), union(~T).with_(F), # "Solving" negation equations rule(eq(~p).to(T)).then(union(p).with_(F)), rule(eq(~p).to(F)).then(union(p).with_(T)), # canonicalize associtivity. "append" for clauses terminate with false rewrite((a | b) | c).to(a | (b | c)), # commutativity rewrite(a | (b | c)).to(b | (a | c)), # absoprtion rewrite(a | (a | b)).to(a | b), rewrite(a | (~a | b)).to(T), # Simplification rewrite(F | a).to(a), rewrite(a | F).to(a), rewrite(T | a).to(T), rewrite(a | T).to(T), # unit propagation # This is kind of interesting actually. # Looks a bit like equation solving rule(eq(T).to(p | F)).then(union(p).with_(T)), # resolution # This counts on commutativity to bubble everything possible up to the front of the clause. rule( eq(T).to(a | as_), eq(T).to(~a | bs), ).then( union(as_ | bs).with_(T), ), ) # Example predicate @function def pred(x: i64Like) -> Boolean: # type: ignore[empty-body] ... p0 = egraph.let("p0", pred(0)) p1 = egraph.let("p1", pred(1)) p2 = egraph.let("p2", pred(2)) egraph.register( union(p1 | (~p2 | F)).with_(T), union(p2 | (~p0 | F)).with_(T), union(p0 | (~p1 | F)).with_(T), union(p1).with_(F), union(~p0 | (~p1 | (p2 | F))).with_(T), ) egraph.run(10) egraph.check(ne(T).to(F)) egraph.check(eq(p0).to(F)) egraph.check(eq(p2).to(F)) egraph .. rst-class:: sphx-glr-timing **Total running time of the script:** (0 minutes 0.050 seconds) .. _sphx_glr_download_auto_examples_resolution.py: .. only:: html .. container:: sphx-glr-footer sphx-glr-footer-example .. container:: sphx-glr-download sphx-glr-download-jupyter :download:`Download Jupyter notebook: resolution.ipynb ` .. container:: sphx-glr-download sphx-glr-download-python :download:`Download Python source code: resolution.py ` .. only:: html .. rst-class:: sphx-glr-signature `Gallery generated by Sphinx-Gallery `_