Unification is a logical flavored word for the notion of equation solving.

Any method for solving unification problems can be basically plugged black box into the applications of type inference (hindley milner stuff), prolog, minikanren, resolution theorem proving, and knuth bendix proving.

SMT solvers are super useful and intrinsically support arithmetic and other cool things. They return ground models however which are too specific to be the desired solutions to unification problems.

A question: How can one use an SMT solver to return a more general unification solution? I have some ideas.

Using an SMT solvers as a boolean propagator

Propagation is an essential pieces of SMT solving. The theory specific solvers have mechanisms to cheaply propagate information from the current assumptions. These are things like tightened inequality bounds implying other bounds, propagation of equality facts through congruence, unit propagation etc. https://www.youtube.com/watch?v=tETbivwzXBM

Once propagation has stopped learning anything (reached a fixed point) to make more progress perhaps you need to branch on a boolean variable, which enables more propagation.

It is somewhat unfortunate that these bare propagation mechanisms are not available to end users. However, using block box smt queries, we can do some propagation from the outside at some extra overhead.

Given a pile of facts we think might be implied by an assertion, we can filter out the ones which have models for which they are false. Another way of putting it is this means the set constrained by the result is a subset of the assertion.

In this manner we can probe the SMT solver to do bounds propagation, congruence closure, etc for us, just so long as we can enumerate the facts we might like to be propagated.

from kdrag.all import *

def propagate(maybes: list[smt.BoolRef], known: smt.BoolRef) -> list[smt.BoolRef]:
    """
    Prune the list of maybes to the ones implies by known

    >>> p,q,r = smt.Bools("p q r")
    >>> propagate([p, q, r, smt.And(p,q)], p & q)
    [p, q, And(p, q)]
    """
    s = smt.Solver()
    s.add(known)
    maybes = list(maybes)
    while True:
        res = s.check()
        if res == smt.unsat:
            return maybes # known = False implies everything. Maybe this should just raise instead.
        assert res == smt.sat
        m = s.model()
        maybes = [e for e in maybes if smt.is_true(m.eval(e))]
        s.add(smt.Not(smt.And(maybes))) # try to make one of the remaining maybes false

x,y,z = smt.Ints("x y z")
vs = [x,y,z]
propagate([v1 <= v2 for v1 in vs for v2 in vs], smt.And(x <= y, y <= z))

[x <= x, x <= y, x <= z, y <= y, y <= z, z <= z]

Bottom Up E-unification

Ok, so here’s a dumb method that can work. Somehow generate a pile of candidate substitution equations v = t and use the solver to propagate the ones that are valid.

The “somehow” is the tough part. One simple method is to offer every possible subterm in the unification problem as a candidate t. For first order syntactic unification (theory of algebraic datatypes) this should always work, for other’s it may only sometimes succeed.

The returned substitution is the most general because it’s implied by the goal. The returned substitution may be “insufficient” though in that we just haven’t suggested a good enough candidate. In this case, we cannot just throw away the goal and must consider the substitution to be a substitution with a remainder of constraints. This is sort of a “dynamic” version of Constraint Logic Programming’s (CLP) distinction between unification-y stuff and constraint stuff.

from kdrag.all import *
from typing import Optional
def eunify(vs : list[smt.ExprRef], goal : smt.BoolRef, term_gen_heuristic=None) -> Optional[tuple[dict[smt.ExprRef, smt.ExprRef], Optional[smt.BoolRef]]]:
    # check that the goal is even solvable at all
    s = smt.Solver()
    s.add(goal)
    res = s.check()
    if res == smt.unsat:
        return None
    elif res == smt.unknown:
        raise Exception("eunify: SMT solver returned unknown")
    assert res == smt.sat
    # solve for ground constants first
    m = s.model()
    guesses = [smt.Eq(v, m.eval(v)) for v in vs if not v.eq(m.eval(v))]
    eqs = kd.utils.propagate(guesses, goal)
    subst = {eq.arg(0): eq.arg(1) for eq in eqs}
    goal = smt.substitute(goal, list(subst.items()))
    # Now guess seed expressions from the goal
    guess_ts = set(kd.utils.subterms(goal))
    # simplify can sometimes generate new subterms (reassociation etc). Questionably useful
    guess_ts.update(kd.utils.subterms(smt.simplify(goal))) 
    # Could perhaps call some z3.Tactics here to generate more terms
    if term_gen_heuristic is not None:
        guess_ts.update(term_gen(vs, goal))
    guesses = [smt.Eq(v, t) for t in guess_ts for v in vs if t.sort() == v.sort() and kd.utils.free_in(v, t)]
    eqs = kd.utils.propagate(guesses, goal)
    while eqs:
        eq = eqs.pop()
        v,t = eq.children()
        if v not in subst and kd.utils.free_in(v, t): # is it possible for free_in to fail? But it to eventually not fail?
            subst[v] = t
            eqs = [smt.substitute(m, (v, t)) for m in eqs if not m.arg(0).eq(v)]
    remainder_constraint = smt.simplify(smt.substitute(goal, *subst.items()))
    return subst, remainder_constraint if not smt.is_true(remainder_constraint) else None

For this example, the model produces a complete substitution

eunify([x,y], smt.And(x + 1 == y, y + 1 == 3))

({x: 1, y: 2}, None)

An incomplete example where we gain some info, but not enough to constrain to the goal

eunify([x,y,z], smt.And(x + y == z, z + 1 + y == 3))

({z: x + y}, x + 2*y == 2)

Here we do not have the appropriate seed expression y - 2x to solve for a variable. We could of course do better.

eunify([x,y,z], smt.And(x + y == z + 3*x, z + 1 + y == 3))

({z: -2*x + y}, -2*x + 2*y == 2)

Here is an example using the algebraic datatype theory of IntLists. We can replicate first order syntactic unification

import kdrag.theories.list as list_

IntList = list_.ListSort(smt.IntSort())
a,b,c = smt.Consts("a b c", IntList)
eunify([a,b,c], smt.And(IntList.Cons(3, a) == IntList.Cons(3, c), IntList.Cons(3,b) == IntList.Cons(3,a), c == b))

({c: b, a: b}, None)

eunify([a,b,c], smt.And(IntList.Cons(3, a) == IntList.Cons(3, c), IntList.Cons(3,b) == IntList.Cons(smt.IntVal(5) - 2, IntList.Nil)))

({b: Nil, c: a}, None)

An impossible goal returns None

eunify([a,b,c], smt.And(IntList.Cons(3, a) == IntList.Cons(3, c), IntList.Cons(3,b) == IntList.Cons(2,IntList.Nil)))

We can also get some mild theory solving in there

eunify([a,b,c,x], smt.And(IntList.Cons(3, a) == IntList.Cons(3, c), IntList.Cons(7 + 3*x,b) == IntList.Cons(1 + x,a), c == b))

({x: -3, b: c, a: c}, None)

IntSeq = smt.SeqSort(smt.IntSort())
s,e,m = smt.Consts("s e m", IntSeq)
eunify([s,e,m], smt.And(s + smt.Unit(smt.IntVal(3)) == m + smt.Unit(smt.IntVal(3))))

({s: m}, None)

eunify([s,e,m], smt.And(smt.Unit(smt.IntVal(3)) + s + smt.Unit(smt.IntVal(3)) == m + smt.Unit(smt.IntVal(3))))

({m: Concat(Unit(3), s)}, None)

eunify([s,e,m], smt.And(smt.Unit(smt.IntVal(3)) + (s + smt.Unit(smt.IntVal(3))) == m + smt.Unit(smt.IntVal(3))))

({m: Concat(Unit(3), s)}, None)

Bits and Bobbles

So the whole thing is kind of a cheat. It could work if you magically get the right substitution candidates, but will it? It opens the door to having domain specific candidate generation heuristics.

  • Bolting on sympy.solve into term_gen_heuristic. Also propagate t1 == t2 equations using t1 and t2 pulled from the goal. Add any sympy can interpret and ask to solve for vars. If it can, confirm solution with z3, add it in until fixed point.
  • quantifier elim. Pavel. Unification is an exists problem, a single quantifier. Z3 offers some qe in it’s tactic system, but I’m not sure how to use it here.
  • relationship to cegis, sygus, synthesis, vampire question answering.

First order syntactic unification zips down two tree-like terms in synchrony and finds variable solutions in that way. Mechanically it’s fairly straightforward.

A confusion occurs about whether this zipping requires injectivity and/or algebraic datatypes. It is always true by the principle of congruence that a solution found in this way is a valid solution. It requires an assumption of injectivity to know that these are the only solutions.

In an automated theorem prover = is semantic equality, but in prolog = is syntactic equality. In an automated theorem prover add(0,0) = 0 is a fine axiom or provable theorem, but in prolog add(0,0) = 0 will fail as non-unifiable.

SMT solvers are more like automated theorem provers. To get something like Prolog’s notion of unification, one wants to use algebraic datatypes

I’ve done a number of blog posts about the relationship of z3 and minikanrens. Python is a metalanguage for which smtlib is embedded and manipulated. One can make the choice of pushing search into or out of the meta layer. These are the same manipulations and tricks that appear in both staged metaprogramming like metaocaml or macros and also in the symbolic execution (path explored at the meta) vs bounded model checking (all paths encoded to solve) distinction (if there really is one. It’s a soft and subjective terminology imo but useful if you’re trying to give a name to different approaches).

If a unification problem is too hard, we can instead approach it from above or below. From above, we return solutions for which there is always a way to extend to substitution and goal is solvable. Return an empty solution is an example of this, it is uninformative but true. From below, we can return solutions which guarantee the truthhood of the goal, but for which there might be other solutions. Returning a ground too specific solution would be an example. Ideally, we’d like the from above and below to exactly describe the goal, by respectively narrowing and generalizing. The are containing sets and subsets that are shrinking and growing respectively.

SMT solvers are more model based than syntactical. They say if there is a satisfying model or none. The exact syntactic steps they in principle follow to show this are vague or complicated (which is perhaps why getting proofs out of them into ITPs is tough).

The starting point of unification is usually syntactic first order unification and then working out from there.

From a semantic perspective, first order syntactic unification is weak sauce. There are tons of solutions that won’t be found by this method. It is a retreat we make to stay within the fast and decidable even if it doesn’t actually answer any useful question. We can take this weak notion of solving as a subroutine in a more exhaustive powerful search. This is what happens in resolution / knuth bendix / prolog / minikanren. As a design principle, it is important to only make automatic that which can be extremely reliable.

E-unification kind of can’t be all that reliable except for some pretty special situations because it lets you answer questions that are too interesting. The one-off reliable situations are mostly too complicated for how specialized they are.

Prolog does not really use the terminology of algebraic data types. The concrete syntax is flavored like and inherited from untyped resolution theorem provers. That’s fine. maybe even interesting. But by and large Prolog really feels like tree manipulation and not the semantic meaning.

The categorical formulation of terms with vars as functions makes sense as another semantics.

What should the solution of a unification problem be?

Unification returns a substitution for some of the variables in the question problem. Assuming this substitution is enough to guarantee the question problem is true.

A complete set of unifiers is a set of substitutions that describe every possible solution.

In E-unification, these are expensive / intractable to ask for.

The propagation thing asks for an overapproximation substitution. I don’t know of a word for this concept? The stuff it couldn’t solve for can be considered as a constraint a la CLP. CLP has this idea of distinguishing between unification-y stuff and constraint stuff. We could consider this distinguishment a dynamically determined distinction if we use our smt solver

The generalization thing asks for an underapproximating substition. It’s not the mgu most general unifier, but something more specific

Minikanren Using esimp

Minikanren writes clauses as recursive functions.

I’ve done this before using define-fun-rec. https://www.philipzucker.com/minikanren_inside_z3/ Something that gives us more control is using knuckeldragger’s definitional unfolding mechanism (based on z3’s substitute_funs) instead of letting define-fun-rec decide hwo things should go.

The entire minikanren state is represented as the current unfolding of the goal expression. That’s kind of fun.

The branching of minikanren is represented in the Or in the expression.

This is kind of basically an encoding of minikanren into term rewriting. The execution ordering is not specified like it is in typical minikanren interpreters. And since kind of the point of minikanren was fair search, why not?

esimp I think is useful for seeking counterexamples in quickcheck like way in knuckledragger. Getting a general solution doesn’t matter that much

def esimp(vs: list[smt.ExprRef], goal: smt.BoolRef, max_iters=7, timeout=50):
    """
    Simplify and unfold goal while seeking a ground model for vs that is provably a solution.
    This can be used in a minikanren-lite way or to produce counterexamples.
    Does not produce generalized solutions like a prolog would.

    >>> n,x,y = smt.Ints("n x y")
    >>> fact = smt.Function("fact", smt.IntSort(), smt.IntSort())
    >>> fact = kd.define("fact", [n], smt.If(n <= 0, 1, n * fact(n - 1)))
    >>> esimp([x], fact(x) == 6)
    {x: 3}
    """
    for i in range(max_iters):
        goal0 = goal
        goal = smt.simplify(goal)
        goal1 = kd.rewrite.unfold(goal)
        assert isinstance(goal1, smt.BoolRef)  # type checker
        goal = goal1
        s = smt.Solver()
        s.set("timeout", timeout)
        s.add(goal)
        res = s.check()
        if res == smt.unsat:
            return False  # Can't be satisfied. raise?
        elif res == smt.sat:
            # Do loop or generalize here?
            m = s.model()
            subst = {v: m.eval(v) for v in vs}
            sgoal = smt.substitute(goal, *subst.items())
            s = smt.Solver()
            s.set("timeout", timeout)
            s.add(smt.Not(sgoal))
            res = s.check()
            if res == smt.unsat:
                return subst
            else:
                # still satisfiable. Not provably a solution.
                pass
        if goal0.eq(goal):
            # No progress. TODO: Could start eliminating models at this point.
            return None
n,x,y = smt.Ints("n x y")
fact = smt.Function("fact", smt.IntSort(), smt.IntSort())
fact = kd.define("fact", [n], smt.If(n <= 0, 1, n * fact(n - 1)))
esimp([x], fact(x) == 6)

{x: 3}

Anti-unification of Models for Unification

Z3 gives us models, which is sweet.

If we ask for models, they are too concrete for what we want.

We can take the models and start to generalize them using some kind of join. The join of term w/vars is anti-unification

Yea, maybe I need to genuinely implement antiunification, not anti pattern matching.

We don’t have to use the abstract domain of term w/vars. We could use other abstract domains. Try to fit a linear approximation.

Or we could have a growing branching set. When two things can’t be successfully antiunified and stay part of the solution set, we append the to a conjunction list.

def antipattern(xs: list[smt.ExprRef]) -> tuple[list[smt.ExprRef], smt.ExprRef]:
    """
    Anti pattern matching. Given a list of concrete examples, return the most specific pattern that matches them all.
    Returns tuple of list of pattern variables and pattern expression.

    https://arxiv.org/pdf/2302.00277 Anti-unification and Generalization: A Survey
    https://arxiv.org/abs/2212.04596  babble: Learning Better Abstractions with E-Graphs and Anti-Unification
    https://ericlippert.com/2018/10/29/anti-unification-part-1/


    >>> a,b,c,d = smt.Ints("a b c d")
    >>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort())
    >>> g = smt.Function("g", smt.IntSort(), smt.IntSort(), smt.IntSort())
    >>> t1 = f(a,g(a,b))
    >>> t2 = f(c,g(c,d))
    >>> t3 = f(a,g(d,b))
    >>> antipattern([t1,t2])
    ([a!..., b!...], f(a!..., g(a!..., b!...)))
    >>> antipattern([t1,t2,t3])
    ([a!..., a!..., b!...], f(a!..., g(a!..., b!...)))

    """
    # we should key on the tuple of all terms, because we want to return same variable.
    sort = xs[0].sort()
    assert all(
        x.sort() == sort for x in xs
    )  # asking to antiunify terms of different sorts is invalid

    # antisubst is a dictionary that maps tuples of terms to a new variable
    antisubst: dict[tuple[smt.ExprRef, ...], smt.ExprRef] = {}

    def worker(xs):
        x0 = xs[0]
        if all(x.eq(x0) for x in xs):
            return x0
        elif xs in antisubst:
            return antisubst[xs]
        elif all(smt.is_app(x) for x in xs):
            decl, nargs = x0.decl(), x0.num_args()
            if all(decl == x.decl() and nargs == x.num_args() for x in xs):
                args = []
                for bs in zip(*[x.children() for x in xs]):
                    args.append(worker(bs))
                return decl(*args)
            else:
                z = smt.FreshConst(x0.sort(), prefix=decl.name())
                antisubst[xs] = z
                return z
        else:
            raise Exception("Unexpected case in antipattern", xs)

    res = worker(tuple(xs))
    return list(antisubst.values()), res

def eunify_under_approx(v, goal):
    vs = [v]
    pat = v
    models = []
    s = smt.Solver()
    s.add(goal)
    while True:
        res = s.check()
        if res == smt.unsat:
            return vs, pat
        else:
            models.append(s.model().eval(v))
            print(models)
            vs, pat = antipattern(models)
            print(vs, pat)
            s.add(smt.Not(smt.Eq(v, pat)))

eunify_under_approx(x, smt.And(x == 2))

[2]
[] 2





([], 2)

Terms w/ Vars as an Abstract Domain

A term with a variable implicitly represents a set of ground terms.

This is similar to the relationship an Interval data structure (a pair of a lower and uppper bound) has to the set of numbers between those bounds. We have a first order manipulatable computational representation of the thing.

This is also kind of sort of like how a polynomial can approximate a function. To make it tighter, a polynomial should represents the sets of functions for which it is the best polynomial approximation of. This is kind of an odd set.

Not all sets can be described in the nice way we’ve parametrized them. If we want to kind of talk about unions and intersections, the best we can do is a meet and join operation, the best approximations to representations of the union and intersection.