# Path: typpete/src/constants.py
# ALIASES = {
#     'Dict': 'dict',
#     'Set': 'set',
#     'List': 'list',
#     'str': 'str'
# }
# 
# Path: typpete/src/z3_types.py
# class Dummy():
# class DummyOptimize:
# class TypesSolver(Solver):
# class Z3Types:
#     def add_soft(self, *args, **kwargs):
#     def add(self, *args, **kwargs):
#     def __init__(self, tree, solver=None, ctx=None, base_folder='',
#                  type_params:dict=None, class_type_params: dict=None):
#     def add(self, *args, fail_message):
#     def init_axioms(self):
#     def infer_stubs(self, context, infer_func):
#     def new_element_id(self):
#     def new_z3_const(self, name, sort=None):
#     def resolve_annotation(self, annotation, module):
#     def __init__(self, config, solver):
#     def subtype(self, t0, t1):
#     def create_class_tree(all_classes, type_sort):
#     def create_subst_axioms(self, tree):
#     def create_subtype_axioms(self, tree):
# def declare_type_sort(max_tuple_length, max_function_args, classes_to_base, type_vars):
# def create_classes_attributes(type_sort, classes_to_attrs, attributes_map):


from typpete.src.constants import ALIASES
from typpete.src.z3_types import And, Or, Implies, Not
        - List[t] --> t
        - str --> str
        - bytes --> bytes
        - Dict{t1: t2} --> t2
        - Tuple(t1, t2, t3, ..., tn) --> Super(t1, t2, t3, ..., tn)
    """

    # Tuple indexing
    # Assert that 'indexed' can be a tuple of an arbitrary length, where the result is the super-type of its elements.
    t = []
    for cur_len in range(1, len(types.tuples)):
        tuple_args = [getattr(types.type_sort, "tuple_{}_arg_{}".format(cur_len, i + 1))(indexed)
                      for i in range(cur_len)]
        t.append(And(
            indexed == types.tuples[cur_len](*tuple_args),
            *[types.subtype(x, result) for x in tuple_args]
        ))

    t.extend(overloading_axioms(indexed, ind, result, '__getitem__', types))

    return [
        Or(
            [And(indexed == types.dict(types.dict_key_type(indexed), result),
                 types.subtype(ind, types.dict_key_type(indexed))),
             And(types.subtype(ind, types.int), indexed == types.list(result)),
             And(types.subtype(ind, types.int), indexed == types.string, result == types.string),
             And(types.subtype(ind, types.int), indexed == types.bytes, result == types.bytes),
             ]
            + t
        )

# Path: typpete/src/constants.py
# ALIASES = {
#     'Dict': 'dict',
#     'Set': 'set',
#     'List': 'list',
#     'str': 'str'
# }
# 
# Path: typpete/src/z3_types.py
# class Dummy():
# class DummyOptimize:
# class TypesSolver(Solver):
# class Z3Types:
#     def add_soft(self, *args, **kwargs):
#     def add(self, *args, **kwargs):
#     def __init__(self, tree, solver=None, ctx=None, base_folder='',
#                  type_params:dict=None, class_type_params: dict=None):
#     def add(self, *args, fail_message):
#     def init_axioms(self):
#     def infer_stubs(self, context, infer_func):
#     def new_element_id(self):
#     def new_z3_const(self, name, sort=None):
#     def resolve_annotation(self, annotation, module):
#     def __init__(self, config, solver):
#     def subtype(self, t0, t1):
#     def create_class_tree(all_classes, type_sort):
#     def create_subst_axioms(self, tree):
#     def create_subtype_axioms(self, tree):
# def declare_type_sort(max_tuple_length, max_function_args, classes_to_base, type_vars):
# def create_classes_attributes(type_sort, classes_to_attrs, attributes_map):


# Path: typpete/src/z3_axioms.py
from typpete.src.constants import ALIASES
from typpete.src.z3_types import And, Or, Implies, Not

        - List[t] --> t
        - str --> str
        - bytes --> bytes
        - Dict{t1: t2} --> t2
        - Tuple(t1, t2, t3, ..., tn) --> Super(t1, t2, t3, ..., tn)
    """

    # Tuple indexing
    # Assert that 'indexed' can be a tuple of an arbitrary length, where the result is the super-type of its elements.
    t = []
    for cur_len in range(1, len(types.tuples)):
        tuple_args = [getattr(types.type_sort, "tuple_{}_arg_{}".format(cur_len, i + 1))(indexed)
                      for i in range(cur_len)]
        t.append(And(
            indexed == types.tuples[cur_len](*tuple_args),
            *[types.subtype(x, result) for x in tuple_args]
        ))

    t.extend(overloading_axioms(indexed, ind, result, '__getitem__', types))

    return [
        Or(
            [And(indexed == types.dict(types.dict_key_type(indexed), result),
                 types.subtype(ind, types.dict_key_type(indexed))),
             And(types.subtype(ind, types.int), indexed == types.list(result)),
             And(types.subtype(ind, types.int), indexed == types.string, result == types.string),
             And(types.subtype(ind, types.int), indexed == types.bytes, result == types.bytes),
             ]
            + t
        )

    ], Or(