transforms_util.py 文件源码

def rewrite_expr_z3_py_ast(r, is_py_ast=True):
    if verbose and False:
        print('rewrite_expr_z3_py_ast:', r)
    # Rewrites py_ast expression to a str expression that could be used in z3
    # Return (z3_expr_str, z3_varnames)
    z3_expr_str = (py_ast.dump_ast(r) if is_py_ast else r).strip()
    z3_expr_str = z3_expr_str.replace('.', '_').replace('[', '_').replace(']', '_')
    rp = py_ast.get_ast(z3_expr_str).body[0].value
    nodes = py_ast.find_all(rp, ast.UnaryOp)
    while nodes != []:
        node = nodes[0]
        if isinstance(node.op, ast.Not):
            if rp == node:
                rp = py_ast.get_ast('z3.Not(' + py_ast.dump_ast(node.operand) + ')').body[0].value
            else:
                py_ast.replace_node(rp, node, py_ast.get_ast('z3.Not(' + py_ast.dump_ast(node.operand) + ')').body[0].value)
            nodes = py_ast.find_all(rp, ast.UnaryOp)
        else:
            nodes = nodes[1:]

    nodes = py_ast.find_all(rp, ast.BoolOp)
    while nodes != []:
        node = nodes[0]
        if isinstance(node.op, ast.And):
            rp_str = 'z3.And('
            for value in node.values:
                rp_str += py_ast.dump_ast(value) + ', '
            rp_str = rp_str.rstrip(', ')
            rp_str += ')'
            if rp == node:
                rp = py_ast.get_ast(rp_str).body[0].value
            else:
                py_ast.replace_node(rp, node, py_ast.get_ast(rp_str).body[0].value)
        elif isinstance(node.op, ast.Or):
            rp_str = 'z3.Or('
            for value in node.values:
                rp_str += py_ast.dump_ast(value) + ', '
            rp_str = rp_str.rstrip(', ')
            rp_str += ')'
            if rp == node:
                rp = py_ast.get_ast(rp_str).body[0].value
            else:
                py_ast.replace_node(rp, node, py_ast.get_ast(rp_str).body[0].value)
        nodes = py_ast.find_all(rp, ast.BoolOp)

    z3_expr_str = py_ast.dump_ast(rp)

    z3_vars = set()
    for node in py_ast.find_all(rp, ast.Name):
        z3_vars.add(node.id)
    if 'z3' in z3_vars:
        z3_vars.remove('z3')
    return (z3_expr_str, z3_vars)