| 54 | } |
| 55 | |
| 56 | void SMTLib2Interface::reset() |
| 57 | { |
| 58 | m_commands.clear(); |
| 59 | m_context.clear(); |
| 60 | m_commands.setOption("produce-models", "true"); |
| 61 | if (m_queryTimeout) |
| 62 | m_commands.setOption("timeout", std::to_string(*m_queryTimeout)); |
| 63 | m_commands.setLogic("ALL"); |
| 64 | m_context.setTupleDeclarationCallback([&](TupleSort const& tupleSort){ |
| 65 | m_commands.declareTuple( |
| 66 | tupleSort.name, |
| 67 | tupleSort.members, |
| 68 | tupleSort.components |
| 69 | | ranges::views::transform([&](SortPointer const& sort){ return m_context.toSmtLibSort(sort); }) |
| 70 | | ranges::to<std::vector>() |
| 71 | ); |
| 72 | }); |
| 73 | } |
| 74 | |
| 75 | void SMTLib2Interface::push() |
| 76 | { |
nothing calls this directly
no test coverage detected