

def normalize_quantifiers(t):
    '\n    Push universals inside conjunctions and existentials inside\n    disjunctions, and flatten conjunctions and disjunctions\n    '
    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) is 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/original