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

Cache solution for the case where we are not interested in models.

Browse Source
This commit is contained in:
chriseth 2022-02-03 17:58:55 +01:00
parent 8835b95719
commit 0f705c8a82
2 changed files with 33 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
libsolutil/LP.cpp
View File

@ -475,25 +475,17 @@ bool Constraint::operator==(Constraint const& _other) const
return true;
}
bool SolvingState::operator<(SolvingState const& _other) const
bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const
{
if (variableNames == _other.variableNames)
if (!considerVariableNames || _a.variableNames == _b.variableNames)
{
if (bounds == _other.bounds)
return constraints < _other.constraints;
if (_a.bounds == _b.bounds)
return _a.constraints < _b.constraints;
else
return bounds < _other.bounds;
return _a.bounds < _b.bounds;
}
else
return variableNames < _other.variableNames;
}
bool SolvingState::operator==(SolvingState const& _other) const
{
return
variableNames == _other.variableNames &&
bounds == _other.bounds &&
constraints == _other.constraints;
return _a.variableNames < _b.variableNames;
}
namespace
@ -734,6 +726,12 @@ SolvingState ProblemSplitter::next()
return splitOff;
}
LPSolver::LPSolver(bool _supportModels):
m_supportModels(_supportModels),
m_cache(SolvingState::Compare{_supportModels})
{
}
pair<LPResult, map<string, rational>> LPSolver::check(SolvingState _state)
{
normalizeRowLengths(_state);
@ -760,9 +758,7 @@ pair<LPResult, map<string, rational>> LPSolver::check(SolvingState _state)
LPResult lpResult;
vector<rational> solution;
// TODO this actually compares including the variable names.
// If we only compare based on coefficients, we will get way more cache hits.
// The downside is that we need to adjust the model.
auto it = m_cache.find(split);
if (it != m_cache.end())
tie(lpResult, solution) = it->second;
@ -778,7 +774,10 @@ pair<LPResult, map<string, rational>> LPSolver::check(SolvingState _state)
objectives.resize(split.constraints.front().data.size(), rational(bigint(1)));
tie(lpResult, solution) = simplex(split.constraints, move(objectives));
}
m_cache.emplace(move(orig), make_pair(lpResult, solution));
// If we do not support models, do not store it in the cache because
// the variable associations will be wrong.
// Otherwise, it is fine to use the model.
m_cache.emplace(move(orig), make_pair(lpResult, m_supportModels ? solution : vector<rational>{}));
}
switch (lpResult)

22
libsolutil/LP.h
View File

@ -62,8 +62,13 @@ struct SolvingState
std::vector<Bounds> bounds;
std::vector<Constraint> constraints;
bool operator<(SolvingState const& _other) const;
bool operator==(SolvingState const& _other) const;
struct Compare
{
explicit Compare(bool _considerVariableNames = true): considerVariableNames(_considerVariableNames) {}
bool operator()(SolvingState const& _a, SolvingState const& _b) const;
bool considerVariableNames;
};
std::string toString() const;
};
@ -153,17 +158,22 @@ private:
*
* Tries to split a given problem into sub-problems and utilizes a cache to quickly solve
* similar problems.
*
* Can be used in a mode where it does not support returning models. In that case, the
* cache is more efficient.
*/
class LPSolver
{
public:
explicit LPSolver(bool _supportModels = true);
std::pair<LPResult, std::map<std::string, boost::rational<bigint>>> check(SolvingState _state);
private:
// TODO check if the model is requested in production. If not, we do not need to cache it.
// TODO This cache is inefficient because it compares including the variable names.
// See comment in LPSolver::check for details.
std::map<SolvingState, std::pair<LPResult, std::vector<boost::rational<bigint>>>> m_cache;
using CacheValue = std::pair<LPResult, std::vector<boost::rational<bigint>>>;
bool m_supportModels = true;
std::map<SolvingState, CacheValue, SolvingState::Compare> m_cache;
};
}