expr_inferrer.py 文件源码

def _get_elements_type(elts, context, lineno, solver):
    """Return the elements type of a collection"""
    elts_type = solver.new_z3_const("elts")
    if len(elts) == 0:
        return elts_type

    all_types = []
    for i in range(0, len(elts)):
        cur_type = infer(elts[i], context, solver)
        all_types.append(cur_type)

        solver.add(solver.z3_types.subtype(cur_type, elts_type),
                   fail_message="List literal in line {}".format(lineno))

    solver.optimize.add_soft(z3.Or([elts_type == elt for elt in all_types]))
    return elts_type