model interpretation for automated theorem proving with Z3

[vdbrueck]

Hi, does someone know how the model output of Z3 automated theorem prover from Microsoft is interpreted?
The model output (s.model()) contains the following cryptical function description. It is not clear to me what this means. Thanks a lot for any help.

    connected = [else ->
              Or(And(If(Var(0) == Type!val!2,
                        Type!val!2,
                        If(Var(0) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!0,
                     If(Var(1) == Type!val!2,
                        Type!val!2,
                        If(Var(1) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!0),
                 And(If(Var(0) == Type!val!2,
                        Type!val!2,
                        If(Var(0) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!1,
                     If(Var(1) == Type!val!2,
                        Type!val!2,
                        If(Var(1) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!1),
                 And(If(Var(0) == Type!val!2,
                        Type!val!2,
                        If(Var(0) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!1,
                     If(Var(1) == Type!val!2,
                        Type!val!2,
                        If(Var(1) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!2),
                 And(If(Var(0) == Type!val!2,
                        Type!val!2,
                        If(Var(0) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!2,
                     If(Var(1) == Type!val!2,
                        Type!val!2,
                        If(Var(1) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!2),
                 And(If(Var(0) == Type!val!2,
                        Type!val!2,
                        If(Var(0) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!2,
                     If(Var(1) == Type!val!2,
                        Type!val!2,
                        If(Var(1) == Type!val!0,
                           Type!val!0,
                           Type!val!1)) ==
                     Type!val!1))],

The associated code is given here:

    from z3 import *
    s=Solver()
    Type=DeclareSort("Type")
    connected=Function("connected",Type,Type,BoolSort())
    r1=Const("r1",Type)
    r2=Const("r2",Type)
    r3=Const("r3",Type)
    r4=Const("r4",Type)
    x=Const("x",Type)
    y=Const("y",Type)

    w=Function("w",Type,BoolSort())
    o=Function("o",Type,BoolSort())
        
    axioms2=w(r1),o(r2),o(r3),ForAll([x,y],
    Implies(And(w(x),w(y)),connected(x,y))),
    ForAll([x,y],Implies(And(o(x),o(y)),connected(x,y)))]
    s2=Solver()
    s2.add(axioms2)
    s2.check()
    print ("MODEL")<br>
    print (s2.model())<br>