| 83 | } |
| 84 | |
| 85 | void SMTLib2Interface::declareVariable(std::string const& _name, SortPointer const& _sort) |
| 86 | { |
| 87 | smtAssert(_sort); |
| 88 | if (_sort->kind == Kind::Function) |
| 89 | declareFunction(_name, _sort); |
| 90 | else if (!m_context.isDeclared(_name)) |
| 91 | { |
| 92 | m_context.declare(_name, _sort); |
| 93 | m_commands.declareVariable(_name, toSmtLibSort(_sort)); |
| 94 | } |
| 95 | } |
| 96 | |
| 97 | void SMTLib2Interface::declareFunction(std::string const& _name, SortPointer const& _sort) |
| 98 | { |
nothing calls this directly
no test coverage detected