A Kanren abusing Z3 to full extent

z3kanren.py

import operator
from z3 import *

def lift(z3assert):
    def res(s):
        s.push()
        s.add(z3assert)
        if s.is_good():
            yield
        s.pop()
    return res
def lift2(op):
    def res(x,y):
        return lift(op(x,y))
    return res
eq = lift2(operator.__eq__)
# lt = lift2(__lt__)
def conj1(f,g):
    def res(s):
        for _ in f(s):            
            if s.is_good():
                #print(s.model())
                yield from g(s)
    return res
import functools
def conj(*args):
    return functools.reduce( conj1 , args )
def disj1(f,g):
    def res(s):
        # itertools.chain(f(s), g(s))
        yield from f(s) 
        yield from g(s)
    return res
def disj(*args):
    return functools.reduce(disj1, args)
def conde(*args):
    return disj(*map(lambda l: conj(*l), args))
def Zzz(thunk_goal):
    def res(s):
        yield from thunk_goal()(s)
    return res
    
def printmodel(s):
    if s.is_good():
        print(s.model())
    yield
def mempty(s):
    if False:
        yield # trick into making it an iterator?

def run(goal):
    s = Solver()
    s.is_good = lambda : s.check() == sat
    for _ in goal(s):
        #s.check()
        yield s.model()
def run_iterative_deep(goal):
    s = Solver()
    s.is_good = lambda : s.num_scopes() < s.max_depth and s.check() == sat
    for depth in itertools.count(start=1):
        s.max_depth = depth
        for _ in goal(s):
            #s.check()
            yield s.model()
def run1(goal):
    s = Solver()
    for _ in goal(s):
        #s.check()
        return s.model()
def runq(qs, goal):
    s = Solver()
    s.is_good = lambda : s.check() == sat
    for _ in goal(s):
        #s.check()
        m = s.model()
        yield {q: m.eval(q) for q in qs}
#run(conj(eq(x,3), conj(eq(y,4), printmodel)))

x, y = Ints("x y")
ex_goal = conj( disj( eq(x,3) , eq(x,4)   ) , disj( eq(y,5) , eq(y,6))  )
list(run(ex_goal))
ex_goal2 = conde( [eq(x,3) , eq(y,4) ] , 
                  [eq(y,5) , eq(x,6) ] )
list(runq([x,y],ex_goal2))