Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A Kanren abusing Z3 to full extent
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment