terpret_z3.py 文件源码

def visit_Compare(self, node):
        left_term = self.visit(node.left)
        if len(node.comparators) > 1:
            raise Exception("Cannot handle 'foo > bar > baz' comparison in %s"
                            % unparse(node))
        right_term = self.visit(node.comparators[0])
        op = node.ops[0]
        if isinstance(op, ast.Eq):
            if self.__is_bool(left_term) and self.__is_bool(right_term):
                if left_term == True:
                    return right_term
                elif right_term == True:
                    return left_term
                elif left_term == False:
                    return Not(right_term)
                elif right_term == False:
                    return Not(left_term)
            return left_term == right_term
        elif isinstance(op, ast.Lt):
            return left_term < right_term
        elif isinstance(op, ast.LtE):
            return left_term <= right_term
        elif isinstance(op, ast.Gt):
            return left_term > right_term
        elif isinstance(op, ast.GtE):
            return left_term >= right_term
        else:
            raise Exception("Unhandled operators '%s' in %s"
                            % (unparse(op), unparse(node)))