cerc-io/solidity
15
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

Merge pull request #5528 from ethereum/smt_sorts_virtual

Browse Source 
[SMTChecker] Make smt::Sort::operator== virtual
This commit is contained in:
chriseth 2018-11-30 16:48:46 +01:00 committed by GitHub
commit cc00d8172b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 16 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
libsolidity/formal/SolverInterface.h
View File

@ -55,7 +55,7 @@ struct Sort
Sort(Kind _kind): Sort(Kind _kind):
kind(_kind) {} kind(_kind) {}
virtual ~Sort() = default; virtual ~Sort() = default;
bool operator==(Sort const& _other) const { return kind == _other.kind; } virtual bool operator==(Sort const& _other) const { return kind == _other.kind; }
Kind const kind; Kind const kind;
}; };
@ -65,16 +65,22 @@ struct FunctionSort: public Sort
{ {
FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain): FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {} Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {}
bool operator==(FunctionSort const& _other) const bool operator==(Sort const& _other) const override
{ {
if (!Sort::operator==(_other))
return false;
auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
solAssert(_otherFunction, "");
if (domain.size() != _otherFunction->domain.size())
return false;
if (!std::equal( if (!std::equal(
domain.begin(), domain.begin(),
domain.end(), domain.end(),
_other.domain.begin(), _otherFunction->domain.begin(),
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; } [&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
)) ))
return false; return false;
return Sort::operator==(_other) && *codomain == *_other.codomain; return *codomain == *_otherFunction->codomain;
} }
std::vector<SortPointer> domain; std::vector<SortPointer> domain;
@ -87,9 +93,13 @@ struct ArraySort: public Sort
/// _range is the sort of the values /// _range is the sort of the values
ArraySort(SortPointer _domain, SortPointer _range): ArraySort(SortPointer _domain, SortPointer _range):
Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {} Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {}
bool operator==(ArraySort const& _other) const bool operator==(Sort const& _other) const override
{ {
return Sort::operator==(_other) && *domain == *_other.domain && *range == *_other.range; if (!Sort::operator==(_other))
return false;
auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
solAssert(_otherArray, "");
return *domain == *_otherArray->domain && *range == *_otherArray->range;
} }
SortPointer domain; SortPointer domain;