terpret_z3.py 文件源码

def visit_BoolOp(self, node):
        if len(node.values) != 2:
            raise Exception("Can only handle binary bool operations at this point: %s"
                            % unparse(node))
        left_term = self.visit(node.values[0])
        right_term = self.visit(node.values[1])

        # 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)

        if isinstance(node.op, ast.And):
            return And(left_term, right_term)
        elif isinstance(node.op, ast.Or):
            return Or(left_term, right_term)
        else:
            raise Exception("Unsupported bool operation %s" % unparse(node))