Rule Synthesis Etudes for Tao's Algebra Problem

Terence Tao had an interesting challenge recently. https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/ https://www.philipzucker.com/tao_algebra/

Others have pointed out there is some similarity to Ruler.

• https://github.com/uwplse/ruler
• https://dl.acm.org/doi/10.1145/3622834 Equality Saturation Theory Exploration à la Carte
• https://dl.acm.org/doi/abs/10.1145/3485496 Rewrite rule inference using equality saturation

Because of this, I thought I’d give rule synthesis a shot today. I don’t think I made it to a fully satisfying solution, but I can’t let myself be too intimated by the one day blog post to not try.

What is Ruler

Ruler is a tool for synthesizing rewrite rules. It, and other tools, does so by smart enumeration. Basically,

1. enumerate terms
2. generate candidate rules as pairs of terms
3. check candidate rules (probably using an SMT solver), reduce redundancy

In our case for Tao’s problem we enumerate candidate equational laws, pair them up into implications rather than rewrite rules. This is kind of one layer up, since we need to

1. enumerate terms
2. generate possible equational axioms as pairs of terms
3. generate equational axiom implication as pairs of axioms

A lot of domain specific smarts can and probably has to go into enumeration of terms. There are too many dang terms. Here are some nice posts in the context of compilers

• https://pypy.org/posts/2024/07/finding-simple-rewrite-rules-jit-z3.html Great Blog post by CF Bolz-Tereick
• https://dl.acm.org/doi/pdf/10.1145/3649837 Hydra: Generalizing Peephole Optimizations with Program Synthesis

Generating candidate rules can just be the $n^2$ pairs of terms

You can prune the search space by

1. using concrete models / inputs to partition definitely disequal expressions. Don’t bother pairing these
2. collapse terms that are already provably equivalent as in Ruler. We could apply this idea in this equational implication context. There are strongly connected components of the implication graph that we could collapse.

Brute Force

Let’s look at how this might look brute force wise.

The is a simple enumerator of terms made of a binary operator m. The general strategy of having a growing set is a useful one. I think of it as datalog-y, but if that doesn’t illuminate anything for you, don’t worry about it.

from z3 import *
T = DeclareSort("T")
vs = Consts("x y z", T)
m = Function("m", T, T, T)

def genterms(n):
    terms = set(vs)
    for j in range(n):
        new = []
        for x in terms:
            for y in terms:
                t = m(x,y)
                if t not in terms:
                    new.append(t)
        terms.update(new)
    return terms
print(len(genterms(3)))

21612

The brute force size of these things quickly brings you to your knees. Note, some of these really should be alpha equivalent.

Anyway, let’s fill these out to build possible equational laws we could talk about for magmas https://en.wikipedia.org/wiki/Magma_(algebra)

from z3 import *
terms = list(genterms(2))
eqs = []
for i,t1 in enumerate(terms):
    for t2 in terms[:i]:
        if not t1.eq(t2):
            eqs.append(ForAll(vs, t1 == t2))
print("neqs", len(eqs), "nterms", len(terms)) 

# maybe we want to alpha reduce here

neqs 10731 nterms 147

And then we can loop through the equations and see which imply each other by calling a black box solver.

These implications do not seem to play well with z3 for some reason, probably they are too quantified. Vampire seems to be crushing them though, so it’s lucky I hooked that up to knuckledragger recently. It is very convenient to be able to just call the solver while reusing the z3 ast and api.

from kdrag.solvers import VampireSolver
from collections import defaultdict

implies = defaultdict(list)

eqs = eqs[:15] # prune
for e1 in eqs:
    for e2 in eqs:
        if not e1.eq(e2):
            s = VampireSolver()
            s.set("timeout", 100)
            s.add(e1)
            s.add(Not(e2))
            res = s.check()
            if res == unsat:
                print("implies", e1, "====>", e2)
                implies[e1].append(e2)
            elif res == sat:
                print("does not imply", e1, "==/=>", e2)
            elif res == unknown:
                print(s.res.stdout.decode())
                print("unknown", e1, e2)

does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
implies ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ====> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
implies ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ====> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ====> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ====> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
implies ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ====> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ====> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ====> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ====> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y))) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z],
       m(m(z, x), m(z, y)) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z], m(m(z, y), z) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z], m(m(z, y), z) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, z), m(x, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, x), m(z, y)))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ==/=> ForAll([x, y, z], m(z, m(x, y)) == m(m(z, y), z))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z], m(m(z, x), y) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z], m(m(z, x), y) == m(m(z, x), m(z, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z], m(m(z, x), y) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ==/=> ForAll([x, y, z], m(m(z, x), y) == m(z, m(x, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, z), m(x, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z],
       m(m(x, y), m(y, x)) == m(m(z, x), m(z, y)))
implies ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ====> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, y), z))
does not imply ForAll([x, y, z], m(m(x, y), m(y, x)) == m(m(z, x), y)) ==/=> ForAll([x, y, z], m(m(x, y), m(y, x)) == m(z, m(x, y)))

That took 4s. It’s not inconceivable to just blast this for hours. It’s also trivially parallelizable. Still, we should look at pruning the brute force method.

https://github.com/teorth/equational_theories Mentions 22 million implications, many of which have already been somewhat easily solved.

Generating Models

We could use models to prune possible candidates. Ruler calls these cvecs

The easiest thing to do is just generate random finite models

Also you can use z3 to generate models.

I would think it is probably not that useful the systematically enumerate models but Mace4 was a prominent model generator which I believe was systematic https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/

import random
def random_model():
    n = random.randint(1, 3)
    return n, { (x,y) : random.randint(0,n-1) for x in range(n) for y in range(n)} # could not use dictionary.

for i in range(5):
    print(random_model())

(3, {(0, 0): 0, (0, 1): 0, (0, 2): 2, (1, 0): 0, (1, 1): 0, (1, 2): 1, (2, 0): 0, (2, 1): 1, (2, 2): 2})
(2, {(0, 0): 0, (0, 1): 1, (1, 0): 0, (1, 1): 0})
(3, {(0, 0): 0, (0, 1): 0, (0, 2): 0, (1, 0): 0, (1, 1): 0, (1, 2): 0, (2, 0): 2, (2, 1): 2, (2, 2): 2})
(1, {(0, 0): 0})
(3, {(0, 0): 2, (0, 1): 0, (0, 2): 0, (1, 0): 1, (1, 1): 1, (1, 2): 0, (2, 0): 1, (2, 1): 1, (2, 2): 0})

import itertools

# TODO: remove permutation symmetry
def all_models():
    n = 0
    while True:
        n += 1
        for f in itertools.product(range(n), repeat=n*n) # n ^ (n^2) combinations
            yield n, { (z // n, z % n) : v for z, v in enumerate(f)}


def all_expr():
    seen = set()
    T = z3.DeclareSort("T")
    vs = set()
    m = z3.Function("m", T,T,T)
    while True:
        seen.add(z3.FreshConst(T, prefix="x"))
        for x in seen:
            for y in seen:
                if m(x,y) not in seen:
                    if m(x,y) not in seen:
                        yield m(x,y)
                        seen.add(m(x,y))
                

AI Generated Rules

Now I’m a little off the trail of the original question

AI based term or rule suggestion. Sure why not.

It’s very fast to do this. It took me like a minute in total. https://chatgpt.com/share/66fb3816-8a70-8008-a8fd-a4622b573c2b

It doesn’t matter if we trust the AI, since z3 can immediately confirm. SOme of the rules the AI spit out do not pass z3. They probably aren’t correct. I commented them out

People have written down bitvector rewrites rules a bunch of times. It’s hard to google for them. But chatgpt probably has them slurped up into its guts.

This might even be useful for knuckledragger, since I can use this to import the theory smarts from z3 over into eprover or others as explicit axiomatic properties.

import kdrag as kd
import kdrag.smt as smt
# TODO: parametrize over the bitwidth
x, y, z = smt.BitVecs("x y z", 32)

bvadd_comm = kd.lemma(smt.ForAll([x, y], x + y == y + x))
bvadd_assoc = kd.lemma(smt.ForAll([x, y, z], (x + y) + z == x + (y + z)))  # Associative property of addition
bvadd_id = kd.lemma(smt.ForAll([x], x + smt.BitVecVal(0, 32) == x))  # Identity element for addition
bvadd_neg = kd.lemma(smt.ForAll([x], x + (-x) == smt.BitVecVal(0, 32)))  # Negation property

bvsub_self = kd.lemma(smt.ForAll([x], x - x == smt.BitVecVal(0, 32)))  # Subtraction of self is zero
bvsub_def = kd.lemma(smt.ForAll([x, y], x - y == x + (-y)))  # Definition of subtraction as addition with negation

bvmul_comm = kd.lemma(smt.ForAll([x, y], x * y == y * x))  # Commutative property of multiplication
bvmul_assoc = kd.lemma(smt.ForAll([x, y, z], (x * y) * z == x * (y * z)))  # Associative property of multiplication
bvmul_id = kd.lemma(smt.ForAll([x], x * smt.BitVecVal(1, 32) == x))  # Identity element for multiplication
bvmul_zero = kd.lemma(smt.ForAll([x], x * smt.BitVecVal(0, 32) == smt.BitVecVal(0, 32)))  # Multiplication by zero

bvand_comm = kd.lemma(smt.ForAll([x, y], x & y == y & x))  # Commutative property of AND
bvand_assoc = kd.lemma(smt.ForAll([x, y, z], (x & y) & z == x & (y & z)))  # Associative property of AND
bvand_id = kd.lemma(smt.ForAll([x], x & smt.BitVecVal(-1, 32) == x))  # Identity element for AND (all bits set)
bvand_zero = kd.lemma(smt.ForAll([x], x & smt.BitVecVal(0, 32) == smt.BitVecVal(0, 32)))  # AND with zero

bvor_comm = kd.lemma(smt.ForAll([x, y], x | y == y | x))  # Commutative property of OR
bvor_assoc = kd.lemma(smt.ForAll([x, y, z], (x | y) | z == x | (y | z)))  # Associative property of OR
bvor_id = kd.lemma(smt.ForAll([x], x | smt.BitVecVal(0, 32) == x))  # Identity element for OR
bvor_neg = kd.lemma(smt.ForAll([x], x | ~x == smt.BitVecVal(-1, 32)))  # OR with negation is all bits set

bvxor_comm = kd.lemma(smt.ForAll([x, y], x ^ y == y ^ x))  # Commutative property of XOR
bvxor_assoc = kd.lemma(smt.ForAll([x, y, z], (x ^ y) ^ z == x ^ (y ^ z)))  # Associative property of XOR
bvxor_id = kd.lemma(smt.ForAll([x], x ^ smt.BitVecVal(0, 32) == x))  # Identity element for XOR
bvxor_self = kd.lemma(smt.ForAll([x], x ^ x == smt.BitVecVal(0, 32)))  # XOR with self is zero

bvshl_zero = kd.lemma(smt.ForAll([x], x << smt.BitVecVal(0, 32) == x))  # Left shift by zero is identity
bvshr_zero = kd.lemma(smt.ForAll([x], smt.LShR(x, smt.BitVecVal(0, 32)) == x))  # Logical right shift by zero is identity

# Bitwise simplification rules
bvand_self = kd.lemma(smt.ForAll([x], x & x == x))  # AND with self is self
bvor_self = kd.lemma(smt.ForAll([x], x | x == x))  # OR with self is self
bvxor_zero = kd.lemma(smt.ForAll([x], x ^ smt.BitVecVal(0, 32) == x))  # XOR with zero is self
bvnot_self = kd.lemma(smt.ForAll([x], ~x == -x - 1))  # NOT of x is equivalent to -x - 1

# Rules for shifting and rotating
bvshl_self = kd.lemma(smt.ForAll([x, y], x << y == x * (smt.BitVecVal(1, 32) << y)))  # Left shift as multiplication
#bvshr_self = kd.lemma(smt.ForAll([x, y], smt.LShR(x, y) == x / (smt.BitVecVal(1, 32) << y)))  # Logical right shift as division
#bvashr_self = kd.lemma(smt.ForAll([x, y], smt.AShr(x, y) == smt.If(x >> 31 == 0, smt.LShR(x, y), ~smt.LShR(~x, y))))  # Arithmetic right shift rule

# Simplification with negation and subtraction
bvsub_zero = kd.lemma(smt.ForAll([x], x - smt.BitVecVal(0, 32) == x))  # Subtraction by zero
bvsub_id = kd.lemma(smt.ForAll([x], smt.BitVecVal(0, 32) - x == -x))  # Zero minus x is negation of x
bvadd_sub = kd.lemma(smt.ForAll([x, y], x + (-y) == x - y))  # Addition of negative is subtraction
bvsub_add = kd.lemma(smt.ForAll([x, y], x - (-y) == x + y))  # Subtraction of negative is addition

# Bitwise AND, OR, and XOR with constants
bvand_allones = kd.lemma(smt.ForAll([x], x & smt.BitVecVal(-1, 32) == x))  # AND with all ones is self
bvor_allzeros = kd.lemma(smt.ForAll([x], x | smt.BitVecVal(0, 32) == x))  # OR with all zeros is self
bvxor_allzeros = kd.lemma(smt.ForAll([x], x ^ smt.BitVecVal(0, 32) == x))  # XOR with all zeros is self

# Distribution and absorption laws
bvand_or = kd.lemma(smt.ForAll([x, y, z], x & (y | z) == (x & y) | (x & z)))  # Distributive law of AND over OR
bvor_and = kd.lemma(smt.ForAll([x, y, z], x | (y & z) == (x | y) & (x | z)))  # Distributive law of OR over AND
bvand_absorb = kd.lemma(smt.ForAll([x, y], x & (x | y) == x))  # Absorption law of AND
bvor_absorb = kd.lemma(smt.ForAll([x, y], x | (x & y) == x))  # Absorption law of OR

# Shifting rules with zero and identity
bvshl_zero_shift = kd.lemma(smt.ForAll([x], x << smt.BitVecVal(0, 32) == x))  # Left shift by zero is identity
bvshr_zero_shift = kd.lemma(smt.ForAll([x], smt.LShR(x, smt.BitVecVal(0, 32)) == x))  # Logical right shift by zero is identity
#bvashr_zero_shift = kd.lemma(smt.ForAll([x], smt.AShr(x, smt.BitVecVal(0, 32)) == x))  # Arithmetic right shift by zero is identity
bvshl_allzeros = kd.lemma(smt.ForAll([y], smt.BitVecVal(0, 32) << y == smt.BitVecVal(0, 32)))  # Left shift of zero is zero
bvshr_allzeros = kd.lemma(smt.ForAll([y], smt.LShR(smt.BitVecVal(0, 32), y) == smt.BitVecVal(0, 32)))  # Logical right shift of zero is zero
#bvashr_allzeros = kd.lemma(smt.ForAll([y], smt.AShr(smt.BitVecVal(0, 32), y) == smt.BitVecVal(0, 32)))  # Arithmetic right shift of zero is zero

# Additional rules for combining operations
#bvadd_and = kd.lemma(smt.ForAll([x, y, z], (x & y) + (x & z) == x & (y + z)))  # AND distribution over addition
bvor_and_not = kd.lemma(smt.ForAll([x, y], (x & y) | (x & ~y) == x))  # Distribution of AND and OR with negation
#bvxor_and_not = kd.lemma(smt.ForAll([x, y], (x & y) ^ (x & ~y) == y))  # Distribution of XOR and AND with negation

# Properties involving shifts and bit manipulations
bvshl_and = kd.lemma(smt.ForAll([x, y, z], (x & y) << z == (x << z) & (y << z)))  # Left shift distribution over AND
bvshr_and = kd.lemma(smt.ForAll([x, y, z], smt.LShR(x & y, z) == smt.LShR(x, z) & smt.LShR(y, z)))  # Logical right shift distribution over AND

Generating Some Real Expressions

So here we’ll play with something a bit closer to a mini Ruler.

As an example, we can generate some real valued expressions.

We start with leaves that are either variables or certain constants.

from z3 import *
from collections import defaultdict
import itertools
leaves =  Consts("a b", RealSort()) + [RealVal(0), RealVal(1), RealVal(-1)]

# Generate terms
terms = set(leaves)
# n = 2 is 10s
for j in range(1):
    new = []
    for x in terms:
        t = Abs(x)
        if t not in terms:
            new.append(t)
        t = -x
        if t not in terms:
            new.append(t)
        for y in terms:
            t = x + y
            if t not in terms:
                new.append(t)
            t = x * y
            if t not in terms:
                new.append(t)
            t = x - y
            if t not in terms:
                new.append(t)
            t = x / y
            if t not in terms:
                new.append(t)
    terms.update(new)

Here’s a mini egraph. I have not implemented ematching, so it can’t use the rules we discover. Also rebuilding is exprensive and possible pointless.

Calling this an egraph may be a bit of stretch. It’s mostly just a union find over the z3 hash cons.

# a mini egraph
uf = {t: t for t in terms}
def find(t):
    if t not in uf: # Is this ok?
        return t
    while not uf[t].eq(t):
        t = uf[t]
    return t
def union(t1, t2):
    t1 = find(t1)
    t2 = find(t2)
    #egraph.add(t1 == t2)
    if not t1.eq(t2):
        uf[t1] = t2
def rebuild():
    for t in terms:
        union(t.decl()(*map(find, t.children())), t)

We have a partition of terms into possible equivalence classes.

We take on of the sets of the partition and if they haven’t all been proved equal, we ask z3. If it finds a countermodel, we refine this sets according the the countermodel.

We can see that the number of iterations of this loop is much less than n^2 because of all the pruning. Most terms are obviously not equal by looking at any random old model.

We can also see the rules I have are junky. I need to implement more of ruler I think or some other method for pruning subsumed rules.

def refine_model(m, part):
    return [list(v) for k,v in itertools.groupby(part, key=lambda t: m.eval(t))]
def find_candidate(part):
    if len(part) == 0: # fast path
        return None
    for t1 in part:
        for t2 in part:
            if find(t1).eq(find(t2)):
                continue
            else:
                return t1, t2
    return None

# sort terms
partitions = [terms]
rules = []
niter = 0
while partitions:
    niter += 1
    part = partitions.pop()
    cands = find_candidate(part)
    if cands is None: # everything in partition is provably equal
        continue
    t1, t2 = cands
    s = Solver()
    s.add(t1 != t2)
    res = s.check()
    if res == sat: # model can distinguish t1 and t2
        m = s.model()
        partitions.extend(refine_model(m, part))
    elif res == unsat:
        union(t1, t2)
        #rebuild()
        rules.append(t1 == t2)
        partitions.append(part)
    else:
        assert False

print("nterms", len(terms), "niter", niter, "nrules", len(rules))
rules

nterms 115 niter 122 nrules 12





[0/1 == 0/-1,
 b - b == a*0,
 -1*-1 == 1 - 0,
 1*-1 == -1*1,
 1*0 == -1*0,
 1 + -1 == -1 + 1,
 b*-1 == 0 - b,
 0*b == b*0,
 0*1 == 0*-1,
 0*1 == 0 - 0,
 0 + b == b + 0,
 1/-1 == -1/1]

Bits and Bobbles

Why am i not just using Ruler off the shelf? Because I’m obstinate and like to do things my way. It’s a learning oppurtunity.

Rule synthesis is trying to synthesize good rewrite rules.

Knuth Bendix completion is “synthesizing” oriented rules out of equations

In this context, we are trying to build a library of useful rewrite rules out of something we have SMT semantics for.

You can reduce redundancy in the rules post hoc by using the simplify rules of knuth bendix completion.

“Theory Exploration” is terminology

Tao’s challenge

Ok, but the Tao problem is about pairs of candidates.

I don’t know that this changes things that much. == is still a term. That evaluates to true and false This is a form of conditional rule learning.

In particular models

The egraph capabilities don’t matter. Also, we can use a z3 boolean model to fast prune. Implications. a => b => c, a => c and we can do the paritioning

First determine all formula equal to each other.

Yikes. That just seems like too many. Let’s take a couple.

eqs = eqs[:10]

for e1, e2 in implies:
    print(e1, "===>\n", e2)

∀x, y, z : m(m(y, x), m(y, x)) = m(z, m(x, y))

!cat /tmp/vampire.smt2

(set-logic ALL)
(declare-sort T 0)
;;declarations
(declare-fun m (T T) T)
;;axioms
(assert (forall ((x T) (y T) (z T)) (= (m (m y x) (m y x)) (m (m z x) y))))
(assert (let ((a!1 (forall ((x T) (y T) (z T))
             (= (m (m y x) (m y x)) (m (m y x) (m z z))))))
  (not a!1)))
(check-sat)

uf = {t: t for t in eqs}
def find(t):
    while uf[t] != t:
        t = uf[t]
    return t
def union(t1, t2):
    t1 = find(t1)
    t2 = find(t2)
    if not t1.eq(t2):
        uf[t1] = t2

partitions = [eqs]
models = []

def find_candidate(part):
    if len(part) == 0: # fast path
        return None
    for t1 in part:
        for t2 in part:
            if find(t1).eq(find(t2)):
                continue
            else:
                return t1, t2
    return None

def refine_partition(m, partitions):
    return [list(v) for part in partitions for k,v in itertools.groupby(part, key=lambda t: m.eval(t))]

while partitions:
    part = partitions.pop()
    s = Solver()
    s.set("timeout", 1000)
    s.add(Not(And([eq1 == eq2 for i,eq1 in enumerate(part) for eq2 in part[:i]])))
    res = s.check()
    if res == sat:
        print("sat")
        m = s.model()
        models.append(m)
        partition = refine_partition(m, partition)
    elif res == unsat:
        for eq in part:
            union(part[0], eq)
    else:
        print(len(part))
        print(part)
        assert False

from z3 import *
import functools
T = DeclareSort("T")
vs = Consts("x y z", T)
m = Function("m", T, T, T)


#@functools.lru_cache # doesn't really help much
@functools.cache # nor does regular chaching 
def depth(e):
    if e.decl() == m:
        return 1 + sum(depth(a) for a in e.children())
    else:
        return 0

terms = set(vs)
for j in range(3):
    new = []
    for x in terms:
        for y in terms:
            t = m(x,y)
            if t not in terms: #and depth(t) <= 4:
                new.append(t)
    #new = [ t for x in seen for y in seen if (t := m(x,y)) not in seen and depth(t) <= 4]
    terms.update(new)
print(len(terms))
#terms[:4]

21612

uf = {t: t for t in terms}
# "egraph" should used undefined sort.
egraph = Solver()
def find(t):
    while uf[t] != t:
        t = uf[t]
    return t
#def canon(t):
#    for t1 in terms:
def union(t1, t2):
    t1 = find(t1)
    t2 = find(t2)
    egraph.add(t1 == t2)
    if not t1.eq(t2):
        uf[t1] = t2


models = []
cvec = {t : [] for t in terms}
for t1 in terms:
    for t2 in terms:
        if find(t1).eq(find(t2)):
            # definitely already equal
            continue
        if cvec[t1] != cvec[t2]:
            # definitely not equal
            continue
        s = Solver()
        s.add(Not(ForAll(vs, t1 == t2)))
        res = s.check()
        if res == sat:
            m = s.model()
            models.append(m)
            for t, v in cvec.items():
                v.append(m.eval(t))
        elif res == unsat:
            union(t1, t2)

from z3 import *
from collections import defaultdict
import itertools
leaves =  Consts("a b", RealSort()) + [RealVal(0), RealVal(1), RealVal(-1)]

# Generate terms
terms = set(leaves)
# n = 2 is 10s
for j in range(1):
    new = []
    for x in terms:
        t = Abs(x)
        if t not in terms:
            new.append(t)
        t = -x
        if t not in terms:
            new.append(t)
        for y in terms:
            t = x + y
            if t not in terms:
                new.append(t)
            t = x * y
            if t not in terms:
                new.append(t)
            t = x - y
            if t not in terms:
                new.append(t)
            t = x / y
            if t not in terms:
                new.append(t)
    terms.update(new)

# a mini egraph
uf = {t: t for t in terms}
def find(t):
    if t not in uf: # Is this ok?
        return t
    while not uf[t].eq(t):
        t = uf[t]
    return t
def union(t1, t2):
    t1 = find(t1)
    t2 = find(t2)
    #egraph.add(t1 == t2)
    if not t1.eq(t2):
        uf[t1] = t2
def rebuild():
    for t in terms:
        union(t.decl()(*map(find, t.children())), t)


def refine_model(m, part):
    return [list(v) for k,v in itertools.groupby(part, key=lambda t: m.eval(t))]
def find_candidate(part):
    if len(part) == 0: # fast path
        return None
    for t1 in part:
        for t2 in part:
            if find(t1).eq(find(t2)):
                continue
            else:
                return t1, t2
    return None

# sort terms
partitions = [terms]
rules = []
niter = 0
while partitions:
    niter += 1
    part = partitions.pop()
    cands = find_candidate(part)
    if cands is None: # everything in partition is provably equal
        continue
    t1, t2 = cands
    s = Solver()
    s.add(t1 != t2)
    res = s.check()
    if res == sat: # model can distinguish t1 and t2
        m = s.model()
        partitions.extend(refine_model(m, part))
    elif res == unsat:
        union(t1, t2)
        #rebuild()
        rules.append(t1 == t2)
        partitions.append(part)
    else:
        assert False

print("nterms", len(terms), "niter", niter, "nrules", len(rules))
rules

nterms 115 niter 122 nrules 12





[0/1 == 0/-1,
 b - b == a*0,
 -1*-1 == 1 - 0,
 1*-1 == -1*1,
 1*0 == -1*0,
 1 + -1 == -1 + 1,
 b*-1 == 0 - b,
 0*b == b*0,
 0*1 == 0*-1,
 0*1 == 0 - 0,
 0 + b == b + 0,
 1/-1 == -1/1]

def abstract_sort(s):
    return DeclareSort(s.name())
def abstract_decl(d : z3.FuncDeclRef):
    return Function(d.name(), [abstract_sort(d.domain(i)) for i in range(d.arity())]  + [abstract_sort(d.range())])
def abstract_expr(t : z3.ExprRef):
        if isinstance(t, z3.RatNumRef):
             
        if is_app(t):
            return abstract_decl(t.decl())(*[abstract_expr(a) for a in t.children()])
        else:
             print(t)
             assert False

abstract_expr(RealVal(1) + RealVal(2))

+(Real, Real)

dir(RealVal(1))
is_int_value(RealVal(1))
is_rational_value(RealVal(1))
type(RealVal(1))

z3.z3.RatNumRef

import functools
T = DeclareSort("T")
a = Const("a", T)
b = Const("b", T)
const = Function("const", RealSort(), T)
add = Function("add", T, T, T)
sub = Function("sub", T, T, T)
mul = Function("mul", T, T, T)
neg = Function("neg", T, T)


leaf_map = {
Const("a", RealSort()) : a,
Const("b", RealSort()) : b,
RealVal(0) : const(0),
RealVal(1) : const(1),
RealVal(-1) : const(-1)
}
q = Const("q", RealSort())
fun_map = {
(q + q).decl() : add,
(q - q).decl() : sub,
(q * q).decl() : mul,
(-q).decl() : neg
}

@functools.cache
def translate(t):
    s = leaf_map.get(t)
    if s is not None:
        return s
    else:
        print(t)
        return fun_map[t.decl()](*map(translate, t.children()))
[translate(t) for t in terms]

b - a
If(a > 0, a, -a)



---------------------------------------------------------------------------

KeyError                                  Traceback (most recent call last)

Cell In[40], line 35
     33         print(t)
     34         return fun_map[t.decl()](*map(translate, t.children()))
---> 35 [translate(t) for t in terms]


Cell In[40], line 35, in <listcomp>(.0)
     33         print(t)
     34         return fun_map[t.decl()](*map(translate, t.children()))
---> 35 [translate(t) for t in terms]


Cell In[40], line 34, in translate(t)
     32 else:
     33     print(t)
---> 34     return fun_map[t.decl()](*map(translate, t.children()))


KeyError: If

Note we are doing much much better than n^2 comparisons. This make sense.

print(len(rules))
rules_old = rules

6884

len(terms)

egraph = Solver()
partitions = []

newpartitions = []
for part in partitions:
    newpart = defaultdict(list)
    for t in part:
        newpart[m.eval(t)].append(t)
    newpartitions.extend(newpart.values())
    




T = DeclareSort("T")
leaves =  Consts("a b c zero one negone", T)
interp = RecFunction("interp", T, RealSort())
interp == 

  Cell In[1], line 50
    interp ==
              ^
SyntaxError: invalid syntax

neqs 10600 nterms 147

eqs

(partial) Knuth bendix completion is a reasonable methodology to minify equations / rewrite rules

use knuck simp

halide case study

Chat GPT

#bvshl_self_safe = kd.lemma(smt.ForAll([x, y], smt.Implies(y >= 0, y < 32, x << y == x * (smt.BitVecVal(1, 32) << y))))
#bvshl_self_safe = kd.lemma(smt.ForAll([x, y], smt.Implies(y >= 0, y < 32, x << y == x * (smt.BitVecVal(1, 32) << y))))