How can i assign (assert) values to functions in Z3py?
Question: I would like to kindly ask , How can I convert the following Z3 constraints
into Z3py (Python API).

    
    
            (declare-datatypes () ((S a b c d e f g)))
    
            (declare-fun fun1 ( S ) Bool)
            (declare-fun fun2 ( S   S ) Bool)
    
    
            (assert (forall ((x S)) (= (fun1 x)
            (or
            (= x  a)
            (= x  b)
            (= x  c)
            (= x  d)
            (= x  e)
            (= x  f)
            (= x g)
            ))))
    
           (assert (forall ((y1 S) (y2 S)) (= (fun2  y1  y2)
           (or
           (and (= y1  a) (= y2  b))
           (and (= y1  c) (= y2  d))
           (and (= y2  e) (= y2  f))
           ))))
    


Answer: 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))
    

