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

Re-add cache.

Browse Source
This commit is contained in:
chriseth 2022-03-24 00:08:28 +01:00
parent 5993cfa732
commit dd1092fda2
4 changed files with 37 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolutil/BooleanLP.cpp
View File

@ -243,7 +243,7 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
// from previous invocations of the boolean solver, we still have to use // from previous invocations of the boolean solver, we still have to use
// a cache. // a cache.
// The current optimization is only for CDCL. // The current optimization is only for CDCL.
lpSolvers.emplace_back(0, LPSolver{}); lpSolvers.emplace_back(0, LPSolver{&m_lpCache});
if ( if (
lpSolvers.back().second.setState(lpState) == LPResult::Infeasible || lpSolvers.back().second.setState(lpState) == LPResult::Infeasible ||
lpSolvers.back().second.check().first == LPResult::Infeasible lpSolvers.back().second.check().first == LPResult::Infeasible

3
libsolutil/BooleanLP.h
View File

@ -122,6 +122,9 @@ private:
/// Stack of state, to allow for push()/pop(). /// Stack of state, to allow for push()/pop().
std::vector<State> m_state{{State{}}}; std::vector<State> m_state{{State{}}};
std::map<SolvingState, LPResult, SolvingState::Compare> m_lpCache;
}; };

34
libsolutil/LP.cpp
View File

@ -506,7 +506,7 @@ bool Constraint::operator<(Constraint const& _other) const
if (rational diff = data.get(i) - _other.data.get(i)) if (rational diff = data.get(i) - _other.data.get(i))
return diff < 0; return diff < 0;
return reasons < _other.reasons; return false;
} }
bool Constraint::operator==(Constraint const& _other) const bool Constraint::operator==(Constraint const& _other) const
@ -518,7 +518,7 @@ bool Constraint::operator==(Constraint const& _other) const
if (data.get(i) != _other.data.get(i)) if (data.get(i) != _other.data.get(i))
return false; return false;
return reasons == _other.reasons; return true;
} }
bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const
@ -912,12 +912,32 @@ pair<LPResult, variant<Model, ReasonSet>> LPSolver::check()
} }
else else
{ {
LinearExpression objectives; optional<LPResult> result;
objectives.resize(1); if (m_cache)
objectives.resize(state.variableNames.size(), rational(bigint(1))); {
// TODO the model relies on the variable numbering. auto it = m_cache->find(state);
tie(problem->result, problem->model) = simplex(state.constraints, move(objectives)); if (it != m_cache->end())
{
//cout << "Cache hit" << endl;
result = it->second;
}
}
if (!result)
{
LinearExpression objectives;
objectives.resize(1);
objectives.resize(state.variableNames.size(), rational(bigint(1)));
// TODO the model relies on the variable numbering.
result = LPResult::Unknown;
tie(*result, problem->model) = simplex(state.constraints, move(objectives));
if (m_cache)
{
(*m_cache)[state] = *result;
//cout << "Cache size " << m_cache->size() << endl;
}
}
problem->dirty = false; problem->dirty = false;
problem->result = *result;
if (problem->result == LPResult::Infeasible) if (problem->result == LPResult::Infeasible)
return {LPResult::Infeasible, reasonSetForSubProblem(*problem)}; return {LPResult::Infeasible, reasonSetForSubProblem(*problem)};
} }

7
libsolutil/LP.h
View File

@ -80,7 +80,7 @@ struct SolvingState
struct Compare struct Compare
{ {
explicit Compare(bool _considerVariableNames = true): considerVariableNames(_considerVariableNames) {} explicit Compare(bool _considerVariableNames = false): considerVariableNames(_considerVariableNames) {}
bool operator()(SolvingState const& _a, SolvingState const& _b) const; bool operator()(SolvingState const& _a, SolvingState const& _b) const;
bool considerVariableNames; bool considerVariableNames;
}; };
@ -179,6 +179,9 @@ class LPSolver
{ {
public: public:
explicit LPSolver(bool _supportModels = true); explicit LPSolver(bool _supportModels = true);
explicit LPSolver(std::map<SolvingState, LPResult, SolvingState::Compare>* _cache):
m_cache(_cache) {}
LPResult setState(SolvingState _state); LPResult setState(SolvingState _state);
void addConstraint(Constraint _constraint); void addConstraint(Constraint _constraint);
@ -209,6 +212,8 @@ private:
std::vector<size_t> m_subProblemsPerConstraint; std::vector<size_t> m_subProblemsPerConstraint;
/// TODO also store the first infeasible subproblem? /// TODO also store the first infeasible subproblem?
/// TODO still retain the cache? /// TODO still retain the cache?
std::map<SolvingState, LPResult, SolvingState::Compare>* m_cache = nullptr;
}; };
} }