diff options
| author | MikolasJanota <MikolasJanota@users.noreply.github.com> | 2021-09-04 00:59:46 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-03 22:59:46 +0000 |
| commit | 5cef06bd2beff38a911c74ec082d9789eed83421 (patch) | |
| tree | a632c89f65c6a0b9cf845e56ac2ac40cc232be5c /src/preprocessing/passes/real_to_int.cpp | |
| parent | 54212c1402e43d3a414d20f3e418f2a0fec10a8d (diff) | |
Avoiding duplicate search in maps (#7055)
This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.
Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
Diffstat (limited to 'src/preprocessing/passes/real_to_int.cpp')
0 files changed, 0 insertions, 0 deletions