| 933 | # -- query --------------------------------------------------------------- |
| 934 | |
| 935 | def query(self, *query: Any) -> CheckSatResult: |
| 936 | q: Any = query[0] if len(query) == 1 else query |
| 937 | if isinstance(q, FuncDeclRef) or not isinstance(q, BoolRef): |
| 938 | self._last_result = unknown |
| 939 | return unknown |
| 940 | |
| 941 | # Build: (premise₁ ∧ … ∧ premiseₙ) → query |
| 942 | goal: BoolRef |
| 943 | if self._premises: |
| 944 | conj = And(*self._premises) if len(self._premises) > 1 else self._premises[0] |
| 945 | goal = Implies(conj, q) |
| 946 | else: |
| 947 | goal = q |
| 948 | |
| 949 | if _try_prove(goal): |
| 950 | self._last_result = sat |
| 951 | return sat |
| 952 | self._last_result = unknown |
| 953 | return unknown |
| 954 | |
| 955 | # -- introspection ------------------------------------------------------- |
| 956 | |