You can encode it in the following way:
from z3 import *
S, (a, b, c, d, e, f, g) = EnumSort('S', ['a', 'b', 'c', 'd', 'e', 'f', 'g'])
fun1 = Function('fun1', S, BoolSort())
fun2 = Function('fun2', S, S, BoolSort())
s = Solver()
x = Const('x', S)
s.add(ForAll([x], fun1(x) == Or(x == a, x == b, x == c, x == d, x == e, x == f, x == g, x == e)))
y1, y2 = Consts('y1 y2', S)
s.add(ForAll([y1, y2], fun2(y1, y2) == Or(And(y1 == a, y2 == b), And(y1 == c, y2 == d), And(y1 == e, y2 == f))))
print(s.check())
print(s.model())
Note that fun1
and fun2
are essentially macros. So, we can avoid the quantifiers and define them as:
def fun1(x):
return Or(x == a, x == b, x == c, x == d, x == e, x == f, x == g, x == e)
def fun2(y1, y2):
return Or(And(y1 == a, y2 == b), And(y1 == c, y2 == d), And(y1 == e, y2 == f))