| 56 | } |
| 57 | |
| 58 | void SMTLib2Context::clear() { |
| 59 | m_functions.clear(); |
| 60 | m_knownTypes.clear(); |
| 61 | m_arraySorts.clear(); |
| 62 | m_tupleSorts.clear(); |
| 63 | m_bitVectorSorts.clear(); |
| 64 | m_callback = {}; |
| 65 | m_knownTypes.emplace_back(std::make_unique<SMTLibSort>(Kind::Bool, std::string("Bool"), std::vector<SortId>{}, SortId{0u})); |
| 66 | m_knownTypes.emplace_back(std::make_unique<SMTLibSort>(Kind::Int, std::string("Int"), std::vector<SortId>{}, SortId{1u})); |
| 67 | assert(m_boolSort == m_knownTypes[0]->id); |
| 68 | assert(m_intSort == m_knownTypes[1]->id); |
| 69 | } |
| 70 | |
| 71 | SortId SMTLib2Context::resolve(SortPointer const& _sort) |
| 72 | { |
no outgoing calls
no test coverage detected