loop_parallel_ast.py 文件源码

def rewrite_expr_z3(r, is_py_ast=True):

    # 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
    for node in py_ast.find_all(rp, ast.UnaryOp):
        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)
    for node in py_ast.find_all(rp, ast.BoolOp):
        if isinstance(node.op, ast.And):
            if rp == node:
                rp = py_ast.get_ast('z3.And(' + py_ast.dump_ast(node.values[0]) + ',' + py_ast.dump_ast(node.values[1]) + ')')
            else:
                py_ast.replace_node(rp, node, py_ast.get_ast('z3.And(' + py_ast.dump_ast(node.values[0]) + ',' + py_ast.dump_ast(node.values[1]) + ')'))
        elif isinstance(node.op, ast.Or):
            if rp == node:
                rp = py_ast.get_ast('z3.Or(' + py_ast.dump_ast(node.values[0]) + ',' + py_ast.dump_ast(node.values[1]) + ')')
            else:
                py_ast.replace_node(rp, node, py_ast.get_ast('z3.Or(' + py_ast.dump_ast(node.values[0]) + ',' + py_ast.dump_ast(node.values[1]) + ')'))
    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)
    return (z3_expr_str, z3_vars)