| 141 | } |
| 142 | |
| 143 | bool EncodingContext::createExpression(frontend::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbVar) |
| 144 | { |
| 145 | solAssert(_e.annotation().type, ""); |
| 146 | if (knownExpression(_e)) |
| 147 | { |
| 148 | expression(_e)->increaseIndex(); |
| 149 | return false; |
| 150 | } |
| 151 | else if (_symbVar) |
| 152 | { |
| 153 | m_expressions.emplace(&_e, _symbVar); |
| 154 | return false; |
| 155 | } |
| 156 | else |
| 157 | { |
| 158 | auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + std::to_string(_e.id()), *this); |
| 159 | m_expressions.emplace(&_e, result.second); |
| 160 | return result.first; |
| 161 | } |
| 162 | } |
| 163 | |
| 164 | bool EncodingContext::knownExpression(frontend::Expression const& _e) const |
| 165 | { |
no test coverage detected