terpret_z3.py 文件源码

def visit_UnaryOp(self, node):
        term = self.visit(node.operand)
        if self.__is_bool(term):
            if isinstance(node.op, ast.Not):
                return Not(term)
            elif isinstance(node.op, ast.Invert):
                return Not(term)
            else:
                raise Exception("Unsupported bool unary operation %s" % unparse(node))

        if DATA_TYPE == "int":
            if isinstance(node.op, ast.USub):
                return -term
            elif isinstance(node.op, ast.Not):
                if is_is_int(term):
                    term = term == IntVal(1)
                return Not(term)
            else:
                raise Exception("Unsupported integer unary operation %s" % unparse(node))
        elif DATA_TYPE.startswith("bit_"):
            if isinstance(node.op, ast.Not):
                return ~term
            elif isinstance(node.op, ast.Invert):
                return ~term
            else:
                raise Exception("Unsupported bitvector unary operation %s" % unparse(node))
        else:
            raise Exception("Unsupported unary operation %s" % unparse(node))