| 579 | return len(self._stack) |
| 580 | |
| 581 | def check(self, *assumptions: BoolRef) -> CheckSatResult: |
| 582 | asserts = list(self._assertions) |
| 583 | asserts.extend(assumptions) |
| 584 | if not asserts: |
| 585 | return sat |
| 586 | conj = And(*asserts) |
| 587 | # Try proving negation → unsat |
| 588 | negated = Not(conj) |
| 589 | if _try_prove(negated): |
| 590 | return unsat |
| 591 | # Try proving conjunction directly → sat (tautologically true) |
| 592 | if _try_prove(conj): |
| 593 | return sat |
| 594 | return unknown |
| 595 | |
| 596 | def model(self) -> ModelRef: |
| 597 | raise NotImplementedError( |