| 796 | __slots__ = ("_quantifier", "_bound", "_body") |
| 797 | |
| 798 | def __init__( |
| 799 | self, |
| 800 | quantifier: str, |
| 801 | bound: list[ExprRef], |
| 802 | body: BoolRef, |
| 803 | ) -> None: |
| 804 | # Build nested ForAllNode/ExistsNode from inside out |
| 805 | bound_names = frozenset( |
| 806 | (v._ast.name, v._sort._ast_sort) for v in bound if isinstance(v._ast, _AstVar) |
| 807 | ) |
| 808 | free = body._vars - bound_names |
| 809 | |
| 810 | # Build the nested AST node |
| 811 | node_cls = ForAllNode if quantifier == "\u2200" else ExistsNode |
| 812 | ast: ASTNode = body._ast |
| 813 | for v in reversed(bound): |
| 814 | ast = node_cls( |
| 815 | name=v._ast.name if isinstance(v._ast, _AstVar) else str(v._ast), |
| 816 | sort=v._sort._ast_sort, |
| 817 | body=ast, |
| 818 | ) |
| 819 | |
| 820 | super().__init__(ast, free) |
| 821 | self._quantifier = quantifier |
| 822 | self._bound = bound |
| 823 | self._body = body |
| 824 | |
| 825 | def body(self) -> BoolRef: |
| 826 | """Return the body of the quantifier.""" |