| 72 | } |
| 73 | |
| 74 | void CHCSmtLib2Interface::registerRelation(Expression const& _expr) |
| 75 | { |
| 76 | smtAssert(_expr.sort); |
| 77 | smtAssert(_expr.sort->kind == Kind::Function); |
| 78 | if (m_context.isDeclared(_expr.name)) |
| 79 | return; |
| 80 | auto const& fSort = std::dynamic_pointer_cast<FunctionSort>(_expr.sort); |
| 81 | smtAssert(fSort->codomain); |
| 82 | auto domain = toSmtLibSort(fSort->domain); |
| 83 | std::string codomain = toSmtLibSort(fSort->codomain); |
| 84 | m_commands.declareFunction(_expr.name, domain, codomain); |
| 85 | m_context.declare(_expr.name, _expr.sort); |
| 86 | } |
| 87 | |
| 88 | void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*_name*/) |
| 89 | { |
no test coverage detected