From e4ad6ef39f25b7d58821ee4e406e7ae3d9d19946 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 24 Mar 2022 01:37:41 +0100 Subject: [PATCH] Use unordered map. --- libsolutil/BooleanLP.h | 2 +- libsolutil/LP.cpp | 8 +++++ libsolutil/LP.h | 79 ++++++++++++++++++++++++++++++++++++++++-- 3 files changed, 86 insertions(+), 3 deletions(-) diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index f4dab298f..85e7efcde 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -123,7 +123,7 @@ private: /// Stack of state, to allow for push()/pop(). std::vector m_state{{State{}}}; - std::map m_lpCache; + std::unordered_map m_lpCache; }; diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index 16e0ed1bd..fa0187a99 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -504,7 +504,11 @@ bool Constraint::operator<(Constraint const& _other) const for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) if (rational diff = data.get(i) - _other.data.get(i)) + { + //cout << "Exit after " << i << endl; return diff < 0; + } + //cout << "full traversal of " << max(data.size(), _other.data.size()) << endl; return false; } @@ -516,7 +520,11 @@ bool Constraint::operator==(Constraint const& _other) const for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) if (data.get(i) != _other.data.get(i)) + { + //cout << "Exit after " << i << endl; return false; + } + //cout << "full traversal of " << max(data.size(), _other.data.size()) << endl; return true; } diff --git a/libsolutil/LP.h b/libsolutil/LP.h index 76b74ff50..31a600edb 100644 --- a/libsolutil/LP.h +++ b/libsolutil/LP.h @@ -24,6 +24,7 @@ #include #include +#include namespace solidity::util { @@ -85,9 +86,83 @@ struct SolvingState bool considerVariableNames; }; + bool operator==(SolvingState const& _other) const noexcept { + return bounds == _other.bounds && constraints == _other.constraints; + } + std::string toString() const; }; +} + +template +inline void hashCombine(std::size_t& _seed, T const& _v) +{ + std::hash hasher; + _seed ^= hasher(_v) + 0x9e3779b9 + (_seed << 6) + (_seed >> 2); +} + +template +inline void hashCombineVector(std::size_t& _seed, std::vector const& _v) +{ + hashCombine(_seed, _v.size()); + for (auto const& x: _v) + hashCombine(_seed, x); +} + +template<> +struct std::hash +{ + std::size_t operator()(solidity::util::SolvingState::Bounds const& _bounds) const noexcept + { + std::size_t result = 0; + hashCombine(result, _bounds.lower); + hashCombine(result, _bounds.upper); + return result; + } +}; + +template<> +struct std::hash +{ + std::size_t operator()(solidity::util::LinearExpression const& _linearExpression) const noexcept + { + std::size_t result = 0; + hashCombine(result, _linearExpression.size()); + for (auto const& x: _linearExpression.enumerate()) + hashCombine(result, x.second); + return result; + } +}; + +template<> +struct std::hash +{ + std::size_t operator()(solidity::util::Constraint const& _constraint) const noexcept + { + std::size_t result = 0; + hashCombine(result, _constraint.equality); + hashCombine(result, _constraint.data); + return result; + } +}; + +template<> +struct std::hash +{ + std::size_t operator()(solidity::util::SolvingState const& _solvingState) const noexcept + { + std::size_t result = 0; + hashCombineVector(result, _solvingState.bounds); + hashCombineVector(result, _solvingState.constraints); + return result; + } +}; + + +namespace solidity::util +{ + enum class LPResult { Unknown, @@ -179,7 +254,7 @@ class LPSolver { public: explicit LPSolver(bool _supportModels = true); - explicit LPSolver(std::map* _cache): + explicit LPSolver(std::unordered_map* _cache): m_cache(_cache) {} @@ -216,7 +291,7 @@ private: std::vector m_subProblemsPerConstraint; /// TODO also store the first infeasible subproblem? /// TODO still retain the cache? - std::map* m_cache = nullptr; + std::unordered_map* m_cache = nullptr; };