Resolution theorem proving.#

%3 outer_cluster_125 cluster_125 outer_cluster_129 cluster_129 outer_cluster_i64-5871781006564002453 cluster_i64-5871781006564002453 outer_cluster_i64-0 cluster_i64-0 outer_cluster_i64-11743562013128004906 cluster_i64-11743562013128004906 pred-0:s->i64-0 pred-5871781006564002453:s->i64-5871781006564002453 pred-11743562013128004906:s->i64-11743562013128004906 Boolean___or__-956477042717034388:s->pred-0 Boolean___or__-956477042717034388:s->pred-5871781006564002453 Boolean___invert__-1143242824664700181:s->T-0 Boolean___or__-3066849178297917964:s->pred-11743562013128004906 Boolean___or__-3066849178297917964:s->Boolean___or__-18000287150597460760 Boolean___or__-18000287150597460760:s->Boolean_FALSE-0 Boolean___or__-18000287150597460760:s->Boolean___or__-18000287150597460760 Boolean___or__-5976664366838553760:s->T-0 Boolean___or__-5976664366838553760:s->Boolean___or__-3066849178297917964 Boolean___invert__-14549606945827793601:s->Boolean___or__-956477042717034388 pred-0 pred i64-0 0 pred-5871781006564002453 pred i64-5871781006564002453 1 pred-11743562013128004906 pred i64-11743562013128004906 2 Boolean___or__-956477042717034388 · | · Boolean___invert__-1143242824664700181 T-0 T Boolean_FALSE-0 Boolean.FALSE Boolean___or__-3066849178297917964 · | · Boolean___or__-18000287150597460760 · | · Boolean___or__-5976664366838553760 · | · Boolean___invert__-14549606945827793601


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

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

Gallery generated by Sphinx-Gallery