| 95 | } |
| 96 | |
| 97 | void SMTLib2Interface::declareFunction(std::string const& _name, SortPointer const& _sort) |
| 98 | { |
| 99 | smtAssert(_sort); |
| 100 | smtAssert(_sort->kind == Kind::Function); |
| 101 | if (!m_context.isDeclared(_name)) |
| 102 | { |
| 103 | auto const& fSort = std::dynamic_pointer_cast<FunctionSort>(_sort); |
| 104 | auto domain = toSmtLibSort(fSort->domain); |
| 105 | std::string codomain = toSmtLibSort(fSort->codomain); |
| 106 | m_context.declare(_name, _sort); |
| 107 | m_commands.declareFunction(_name, domain, codomain); |
| 108 | } |
| 109 | } |
| 110 | |
| 111 | void SMTLib2Interface::addAssertion(Expression const& _expr) |
| 112 | { |
no test coverage detected