terpret_z3.py 文件源码

def visit_BinOp(self, node):
        left_term = self.visit(node.left)
        right_term = self.visit(node.right)

        if self.__is_bool(left_term) and self.__is_bool(right_term):
            if isinstance(node.op, ast.BitAnd):
                return And(left_term, right_term)
            elif isinstance(node.op, ast.BitOr):
                return Or(left_term, right_term)
            elif isinstance(node.op, ast.BitXor):
                return Xor(left_term, right_term)
            else:
                raise Exception("Unsupported bool binary operation %s" % unparse(node))

        if DATA_TYPE == "int":
            if isinstance(node.op, ast.Mod):
                return left_term % right_term
            elif isinstance(node.op, ast.Add):
                return left_term + right_term
            elif isinstance(node.op, ast.Sub):
                return left_term - right_term
            elif isinstance(node.op, ast.Mult):
                return left_term * right_term
            elif isinstance(node.op, ast.BitXor):
                # Special-case for bool circuit-examples:
                if is_is_int(left_term):
                    left_term = left_term == IntVal(1)
                if is_is_int(right_term):
                    right_term = right_term == IntVal(1)
                return left_term != right_term
            else:
                raise Exception("Unsupported integer binary operation %s" % unparse(node))
        elif DATA_TYPE.startswith("bit_"):
            if isinstance(node.op, ast.BitAnd):
                return left_term & right_term
            elif isinstance(node.op, ast.BitOr):
                return left_term | right_term
            elif isinstance(node.op, ast.BitXor):
                return left_term ^ right_term
            else:
                raise Exception("Unsupported bitvector operation %s" % unparse(node))
        else:
            raise Exception("Unsupported data type %s" % DATA_TYPE)