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

Different impl.

Browse Source
This commit is contained in:
chriseth 2022-03-23 17:59:17 +01:00
parent 874a8a4753
commit 0c89ef6863
2 changed files with 46 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
libsolutil/LP.cpp
View File

@ -799,11 +799,13 @@ void LPSolver::setState(SolvingState _state)
cout << "Set state:\n" << _state.toString() << endl; cout << "Set state:\n" << _state.toString() << endl;
m_state = move(_state); m_state = move(_state);
m_subProblems.clear(); m_subProblems.clear();
m_subProblemsPerVariable = {};
m_subProblemsPerConstraintReason = {}; m_subProblemsPerConstraintReason = {};
normalizeRowLengths(m_state); normalizeRowLengths(m_state);
m_subProblemsPerVariable.resize(m_state.variableNames.size(), static_cast<size_t>(-1));
m_subProblemsPerConstraint.resize(m_state.constraints.size(), static_cast<size_t>(-1));
// TODO we should simplify, otherwise we get big problems with constanst that are used everywhere. // TODO we should simplify, otherwise we get big problems with constanst that are used everywhere.
// TODO we could simplify, but then we need the option to answer 'infeasible' here. // TODO we could simplify, but then we need the option to answer 'infeasible' here.
@ -818,14 +820,11 @@ void LPSolver::setState(SolvingState _state)
solAssert(m_subProblems.back()->dirty); solAssert(m_subProblems.back()->dirty);
for (auto&& [i, included]: variables | ranges::views::enumerate) for (auto&& [i, included]: variables | ranges::views::enumerate)
if (included) if (included)
{
m_subProblemsPerVariable[i] = m_subProblems.size() - 1; m_subProblemsPerVariable[i] = m_subProblems.size() - 1;
m_subProblems.back()->variables.emplace(i);
}
for (auto&& [i, included]: constraints | ranges::views::enumerate) for (auto&& [i, included]: constraints | ranges::views::enumerate)
if (included) if (included)
m_subProblems.back()->constraints.emplace(i); m_subProblemsPerConstraint[i] = m_subProblems.size() - 1;
cout << "Adding new sub problem with " << m_subProblems.back()->variables.size() << " vars and " << m_subProblems.back()->constraints.size() << " constraints\n" << endl; //cout << "Adding new sub problem with " << m_subProblems.back()->variables.size() << " vars and " << m_subProblems.back()->constraints.size() << " constraints\n" << endl;
// We do not need t ofill m_subProblemsPerConstraintReason because we do not assume // We do not need t ofill m_subProblemsPerConstraintReason because we do not assume
// these constraints to have reasons, so they cannot be removed. // these constraints to have reasons, so they cannot be removed.
// TODO we cauld assert that // TODO we cauld assert that
@ -867,7 +866,7 @@ pair<LPResult, variant<Model, ReasonSet>> LPSolver::check(
solAssert(constraint.reasons.size() == 1); solAssert(constraint.reasons.size() == 1);
set<size_t> touchedProblems; set<size_t> touchedProblems;
for (auto const& [index, entry]: constraint.data.enumerateTail()) for (auto const& [index, entry]: constraint.data.enumerateTail())
if (entry && m_subProblemsPerVariable.count(index)) if (entry && m_subProblemsPerVariable[index] != static_cast<size_t>(-1))
touchedProblems.emplace(m_subProblemsPerVariable[index]); touchedProblems.emplace(m_subProblemsPerVariable[index]);
if (touchedProblems.empty()) if (touchedProblems.empty())
{ {
@ -880,6 +879,9 @@ pair<LPResult, variant<Model, ReasonSet>> LPSolver::check(
combineSubProblems(*touchedProblems.begin(), problemToErase); combineSubProblems(*touchedProblems.begin(), problemToErase);
addConstraintToSubProblem(*touchedProblems.begin(), move(constraint)); addConstraintToSubProblem(*touchedProblems.begin(), move(constraint));
} }
// TODO here, we split again and also remove empty problems.
// TODO here, we can try to split again. // TODO here, we can try to split again.
// If we split here, then we maybe don't need to split in setState. // If we split here, then we maybe don't need to split in setState.
@ -895,17 +897,17 @@ pair<LPResult, variant<Model, ReasonSet>> LPSolver::check(
void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom) void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom)
{ {
m_subProblems[_combineInto]->dirty = true; m_subProblems[_combineInto]->dirty = true;
// TODO we can make this more efficient by using m_subProblems[_combineFrom]->variables
// and m_subProblems[_combineFrom]->constraints for (size_t& item: m_subProblemsPerVariable)
for (auto& item: m_subProblemsPerVariable) if (item == _combineFrom)
if (item.second == _combineFrom) item = _combineInto;
item.second = _combineInto; for (size_t& item: m_subProblemsPerConstraint)
if (item == _combineFrom)
item = _combineInto;
for (auto& item: m_subProblemsPerConstraintReason) for (auto& item: m_subProblemsPerConstraintReason)
if (item.second == _combineFrom) if (item.second == _combineFrom)
item.second = _combineInto; item.second = _combineInto;
m_subProblems[_combineInto]->variables += m_subProblems[_combineFrom]->variables;
m_subProblems[_combineInto]->constraints += m_subProblems[_combineFrom]->constraints;
m_subProblems[_combineFrom].reset(); m_subProblems[_combineFrom].reset();
} }
@ -914,9 +916,8 @@ void LPSolver::addConstraintToSubProblem(size_t _subProblem, Constraint _constra
for (auto const& [index, entry]: _constraint.data.enumerateTail()) for (auto const& [index, entry]: _constraint.data.enumerateTail())
if (entry) if (entry)
{ {
solAssert(!m_subProblemsPerVariable.count(index) || m_subProblemsPerVariable[index] == _subProblem); solAssert(m_subProblemsPerVariable[index] == static_cast<size_t>(-1) || m_subProblemsPerVariable[index] == _subProblem);
m_subProblemsPerVariable[index] = _subProblem; m_subProblemsPerVariable[index] = _subProblem;
m_subProblems[_subProblem]->variables.insert(index);
} }
solAssert(!_constraint.reasons.empty()); solAssert(!_constraint.reasons.empty());
{ {
@ -929,17 +930,15 @@ void LPSolver::addConstraintToSubProblem(size_t _subProblem, Constraint _constra
void LPSolver::updateSubProblems() void LPSolver::updateSubProblems()
{ {
for (unique_ptr<SubProblem>& problem: m_subProblems) for (auto&& [index, problem]: m_subProblems | ranges::views::enumerate)
{ {
if (problem && problem->constraints.empty() && problem->removableConstraints.empty())
continue;
if (!problem || !problem->dirty) if (!problem || !problem->dirty)
{ {
//cout << "not dirty" << endl; //cout << "not dirty" << endl;
continue; continue;
} }
//cout << "Updating sub problem" << endl; //cout << "Updating sub problem" << endl;
SolvingState state = stateFromSubProblem(*problem); SolvingState state = stateFromSubProblem(index);
normalizeRowLengths(state); normalizeRowLengths(state);
// TODO could also call simplify // TODO could also call simplify
//cout << state.toString() << endl; //cout << state.toString() << endl;
@ -949,6 +948,11 @@ void LPSolver::updateSubProblems()
problem->result = LPResult::Infeasible; problem->result = LPResult::Infeasible;
problem->model = {}; problem->model = {};
} }
else if (state.constraints.empty())
{
problem->result = LPResult::Feasible;
problem->model = {};
}
else else
{ {
LinearExpression objectives; LinearExpression objectives;
@ -963,34 +967,35 @@ void LPSolver::updateSubProblems()
} }
} }
SolvingState LPSolver::stateFromSubProblem(LPSolver::SubProblem const& _problem) const SolvingState LPSolver::stateFromSubProblem(size_t _index) const
{ {
SolvingState split; SolvingState split;
split.variableNames.emplace_back(); split.variableNames.emplace_back();
split.bounds.emplace_back(); split.bounds.emplace_back();
for (size_t i: _problem.variables) for (auto&& item: m_subProblemsPerVariable | ranges::views::enumerate)
{ if (item.second == _index)
split.variableNames.emplace_back(m_state.variableNames[i]); {
split.bounds.emplace_back(m_state.bounds[i]); split.variableNames.emplace_back(m_state.variableNames[item.first]);
} split.bounds.emplace_back(m_state.bounds[item.first]);
}
for (auto&& item: m_subProblemsPerConstraint | ranges::views::enumerate)
if (item.second == _index)
{
Constraint const& constraint = m_state.constraints[item.first];
Constraint splitRow{{}, constraint.equality, constraint.reasons};
for (size_t j = 0; j < constraint.data.size(); j++)
if (j == 0 || m_subProblemsPerVariable[j] == _index)
splitRow.data.push_back(constraint.data[j]);
split.constraints.push_back(move(splitRow));
}
for (size_t i: _problem.constraints) for (Constraint const& constraint: m_subProblems[_index]->removableConstraints)
{
Constraint const& constraint = m_state.constraints[i];
Constraint splitRow{{}, constraint.equality, constraint.reasons};
for (size_t j = 0; j < constraint.data.size(); j++)
if (j == 0 || _problem.variables.count(j))
splitRow.data.push_back(constraint.data[j]);
split.constraints.push_back(move(splitRow));
}
for (Constraint const& constraint: _problem.removableConstraints)
{ {
Constraint splitRow{{}, constraint.equality, constraint.reasons}; Constraint splitRow{{}, constraint.equality, constraint.reasons};
for (size_t j = 0; j < constraint.data.size(); j++) for (size_t j = 0; j < constraint.data.size(); j++)
if (j == 0 || _problem.variables.count(j)) if (j == 0 || m_subProblemsPerVariable[j] == _index)
splitRow.data.push_back(constraint.data[j]); splitRow.data.push_back(constraint.data[j]);
split.constraints.push_back(move(splitRow)); split.constraints.push_back(move(splitRow));
} }

12
libsolutil/LP.h
View File

@ -196,25 +196,19 @@ private:
SolvingState m_state; SolvingState m_state;
struct SubProblem struct SubProblem
{ {
// TODO maybe it is better have a single vector of size_t that juts
// specifies which subproblem the variable belongs to.
// we need to traverse the variable vector anywoy.
// same for constraints.
std::set<size_t> variables;
/// This is an index into the constraint vector of m_state.
std::set<size_t> constraints;
std::vector<Constraint> removableConstraints; std::vector<Constraint> removableConstraints;
bool dirty = true; bool dirty = true;
LPResult result = LPResult::Unknown; LPResult result = LPResult::Unknown;
std::vector<boost::rational<bigint>> model = {}; std::vector<boost::rational<bigint>> model = {};
}; };
SolvingState stateFromSubProblem(SubProblem const& _problem) const; SolvingState stateFromSubProblem(size_t _index) const;
ReasonSet reasonSetForSubProblem(SubProblem const& _subProblem); ReasonSet reasonSetForSubProblem(SubProblem const& _subProblem);
// TODO we could also use optional // TODO we could also use optional
std::vector<std::unique_ptr<SubProblem>> m_subProblems; std::vector<std::unique_ptr<SubProblem>> m_subProblems;
std::map<size_t, size_t> m_subProblemsPerVariable; std::vector<size_t> m_subProblemsPerVariable;
std::vector<size_t> m_subProblemsPerConstraint;
/// The key of this is a constraint reason, not an index in the state. /// The key of this is a constraint reason, not an index in the state.
std::map<size_t, size_t> m_subProblemsPerConstraintReason; std::map<size_t, size_t> m_subProblemsPerConstraintReason;
/// TODO also store the first infeasible subproblem? /// TODO also store the first infeasible subproblem?