cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix parsing of let expression to allow shadowing values

Browse Source
This commit is contained in:
Martin Blicha 2023-07-26 17:40:02 +02:00
parent 92689e4256
commit 9339b7074a
1 changed files with 15 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -454,7 +454,8 @@ namespace
}; };
struct LetBindings { struct LetBindings {
std::unordered_map<std::string, SMTLib2Expression> bindings; using BindingRecord = std::vector<SMTLib2Expression>;
std::unordered_map<std::string, BindingRecord> bindings;
std::vector<std::string> varNames; std::vector<std::string> varNames;
std::vector<std::size_t> scopeBounds; std::vector<std::size_t> scopeBounds;
@ -467,7 +468,8 @@ namespace
{ {
auto it = bindings.find(varName); auto it = bindings.find(varName);
assert(it != bindings.end()); assert(it != bindings.end());
return it->second; assert(!it->second.empty());
return it->second.back();
} }
void pushScope() void pushScope()
@ -483,7 +485,11 @@ namespace
auto const& varName = varNames.back(); auto const& varName = varNames.back();
auto it = bindings.find(varName); auto it = bindings.find(varName);
assert(it != bindings.end()); assert(it != bindings.end());
bindings.erase(it); auto & record = it->second;
record.pop_back();
if (record.empty()) {
bindings.erase(it);
}
varNames.pop_back(); varNames.pop_back();
} }
scopeBounds.pop_back(); scopeBounds.pop_back();
@ -491,8 +497,12 @@ namespace
void addBinding(std::string name, SMTLib2Expression expression) void addBinding(std::string name, SMTLib2Expression expression)
{ {
assert(!has(name)); auto it = bindings.find(name);
bindings.insert({name, std::move(expression)}); if (it == bindings.end()) {
bindings.insert({name, {std::move(expression)}});
} else {
it->second.push_back(std::move(expression));
}
varNames.push_back(std::move(name)); varNames.push_back(std::move(name));
} }
}; };