octagon_domain.py 文件源码

 复制代码def __repr__(self):
        if self.is_bottom():
            return "?"
        elif self.is_top():
            return "?"
        else:
            res = []
            # represent unary constraints first
            for var in self.variables:
                lower = - self[PLUS, var, MINUS, var] // 2
                upper = self[MINUS, var, PLUS, var] // 2
                if lower < inf and upper < inf:
                    res.append(f"{lower}?{var.name}?{upper}")
                elif lower < inf:
                    res.append(f"{lower}?{var.name}")
                elif upper < inf:
                    res.append(f"{var.name}?{upper}")
            # represent binary constraints second, do not repeat identical inequalities
            for i, var1 in enumerate(self.variables):
                for j, var2 in enumerate(self.variables):
                    if i > j:
                        c = self[MINUS, var1, PLUS, var2]
                        if c < inf:
                            res.append(f"{var1.name}+{var2.name}?{c}")
                        c = self[MINUS, var1, MINUS, var2]
                        if c < inf:
                            res.append(f"{var1.name}-{var2.name}?{c}")
                        c = self[PLUS, var1, PLUS, var2]
                        if c < inf:
                            res.append(f"-{var1.name}+{var2.name}?{c}")
                        c = self[PLUS, var1, MINUS, var2]
                        if c < inf:
                            res.append(f"-{var1.name}-{var2.name}?{c}")
            return ", ".join(res)