aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--libsolidity/formal/SolverInterface.h22
1 files changed, 16 insertions, 6 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 7f20876e..4a4b3fb1 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -55,7 +55,7 @@ struct Sort
Sort(Kind _kind):
kind(_kind) {}
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;
};
@@ -65,16 +65,22 @@ struct FunctionSort: public Sort
{
FunctionSort(std::vector<SortPointer> _domain, SortPointer _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(
domain.begin(),
domain.end(),
- _other.domain.begin(),
+ _otherFunction->domain.begin(),
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
))
return false;
- return Sort::operator==(_other) && *codomain == *_other.codomain;
+ return *codomain == *_otherFunction->codomain;
}
std::vector<SortPointer> domain;
@@ -87,9 +93,13 @@ struct ArraySort: public Sort
/// _range is the sort of the values
ArraySort(SortPointer _domain, SortPointer _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;