Quantified expression (ForAll / Exists).
| 791 | |
| 792 | |
| 793 | class QuantifierRef(BoolRef): |
| 794 | """Quantified expression (ForAll / Exists).""" |
| 795 | |
| 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.""" |
| 827 | return self._body |
| 828 | |
| 829 | def is_forall(self) -> bool: |
| 830 | return self._quantifier == "\u2200" |
| 831 | |
| 832 | def is_exists(self) -> bool: |
| 833 | return self._quantifier == "\u2203" |
| 834 | |
| 835 | def num_vars(self) -> int: |
| 836 | """Return the number of bound variables.""" |
| 837 | return len(self._bound) |
| 838 | |
| 839 | def var_name(self, i: int) -> str: |
| 840 | """Return the name of the i-th bound variable.""" |
| 841 | v = self._bound[i] |
| 842 | if isinstance(v._ast, _AstVar): |
| 843 | return v._ast.name |
| 844 | return str(v._ast) |
| 845 | |
| 846 | def var_sort(self, i: int) -> SortRef: |
| 847 | """Return the sort of the i-th bound variable.""" |
| 848 | return self._bound[i]._sort |
| 849 | |
| 850 | def weight(self) -> int: |