def normalize_quantifiers(t):
    """
    Push universals inside conjunctions and existentials inside
    disjunctions, and flatten conjunctions and disjunctions
    """

    if type(t) in (Var, Const):
        return t

    elif type(t) in (Apply, Eq, Ite, Not, Implies, Iff):
        return type(t)(*(normalize_quantifiers(x) for x in t))

    elif type(t) in (And, Or):
        return type(t)(*(
            z
            for x in t
            for y in [normalize_quantifiers(x)]
            for z in (y if type(y) is type(t) else [y])
        ))

    elif ((type(t) is ForAll and type(t.body) == And) or
          (type(t) is Exists and type(t.body) is Or)):
        return normalize_quantifiers(type(t.body)(*(
            type(t)(t.variables, x)
            for x in t.body
        )))

    elif type(t) in (ForAll, Exists):
        return type(t)(free_variables(t.body) & frozenset(t.variables),
                       normalize_quantifiers(t.body))

    else:
        assert False, type(t)
dataset/ETHPy150Open Microsoft/ivy/ivy/logic_util.py/normalize_quantifiers/operator `is` -> `==`