stmt_inferrer.py 文件源码

def _infer_assignment_target(target, context, value_type, solver):
    """Infer the type of a target in an assignment

    Attributes:
        target: the target whose type is to be inferred
        context: the current context level
        value_type: the type of the value assigned to the target

    Target cases:
        - Variable name. Ex: x = 1
        - Tuple. Ex: a, b = 1, "string"
        - List. Ex: [a, b] = [1, "string"]
        - Subscript. Ex: x[0] = 1, x[1 : 2] = [2,3], x["key"] = value
        - Compound: Ex: a, b[0], [c, d], e["key"] = 1, 2.0, [True, False], "value"
    """
    target_type = _infer_one_target(target, context, solver)
    solver.add(axioms.assignment(target_type, value_type, solver.z3_types),
               fail_message="Assignment in line {}".format(target.lineno))

    # Adding weight of 2 to give the assignment soft constraint a higher priority over others.
    solver.optimize.add_soft(target_type == value_type, weight=2)