terpret_z3.py 文件源码

def visit_If(self, if_node):
        exprVisitor = ToZ3ExprVisitor(env=self.__env)
        test_term = exprVisitor.visit(if_node.test)
        then_constraints = list(itertools.chain.from_iterable([
            self.visit(stmt) for stmt in if_node.body]))
        else_constraints = list(itertools.chain.from_iterable([
            self.visit(stmt) for stmt in if_node.orelse]))
        then_constraint = then_constraints[0] if len(then_constraints) == 1 else And(then_constraints)
        else_constraint = else_constraints[0] if len(else_constraints) == 1 else And(else_constraints)

        if len(else_constraints) == 0:
            return [Implies(test_term, then_constraint)]
        else:
            return [Implies(test_term,      then_constraint),
                    Implies(Not(test_term), else_constraint)]