| 1495 | |
| 1496 | |
| 1497 | TypingAssignments::TypingAssignments(const expr &e) : s(true), sneg(true) { |
| 1498 | if (e.isTrue()) { |
| 1499 | has_only_one_solution = true; |
| 1500 | } else { |
| 1501 | EnableSMTQueriesTMP tmp; |
| 1502 | s.add(e); |
| 1503 | sneg.add(!e); |
| 1504 | r = s.check("typing"); |
| 1505 | } |
| 1506 | } |
| 1507 | |
| 1508 | TypingAssignments::operator bool() const { |
| 1509 | return !is_unsat && (has_only_one_solution || r.isSat()); |