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

Improved reason computation.

Browse Source
This commit is contained in:
chriseth 2022-05-30 19:00:06 +02:00
parent faa3a242ee
commit 0a4f4f6f55
2 changed files with 58 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
libsolutil/LP.cpp
View File

@ -231,7 +231,7 @@ void LPSolver::setVariableName(size_t _variable, string _name)
p.variables[p.varMapping.at(_variable)].name = move(_name); p.variables[p.varMapping.at(_variable)].name = move(_name);
} }
void LPSolver::addLowerBound(size_t _variable, RationalWithDelta _bound) void LPSolver::addLowerBound(size_t _variable, RationalWithDelta _bound, optional<size_t> _reason)
{ {
SubProblem& p = unsealForVariable(_variable); SubProblem& p = unsealForVariable(_variable);
size_t innerIndex = p.varMapping.at(_variable); size_t innerIndex = p.varMapping.at(_variable);
@ -239,11 +239,12 @@ void LPSolver::addLowerBound(size_t _variable, RationalWithDelta _bound)
if (!var.bounds.lower || *var.bounds.lower < _bound) if (!var.bounds.lower || *var.bounds.lower < _bound)
{ {
var.bounds.lower = move(_bound); var.bounds.lower = move(_bound);
var.bounds.lowerReason = move(_reason);
p.variablesPotentiallyOutOfBounds.insert(innerIndex); p.variablesPotentiallyOutOfBounds.insert(innerIndex);
} }
} }
void LPSolver::addUpperBound(size_t _variable, RationalWithDelta _bound) void LPSolver::addUpperBound(size_t _variable, RationalWithDelta _bound, optional<size_t> _reason)
{ {
SubProblem& p = unsealForVariable(_variable); SubProblem& p = unsealForVariable(_variable);
size_t innerIndex = p.varMapping.at(_variable); size_t innerIndex = p.varMapping.at(_variable);
@ -251,6 +252,7 @@ void LPSolver::addUpperBound(size_t _variable, RationalWithDelta _bound)
if (!var.bounds.upper || *var.bounds.upper > _bound) if (!var.bounds.upper || *var.bounds.upper > _bound)
{ {
var.bounds.upper = move(_bound); var.bounds.upper = move(_bound);
var.bounds.upperReason = move(_reason);
p.variablesPotentiallyOutOfBounds.insert(innerIndex); p.variablesPotentiallyOutOfBounds.insert(innerIndex);
} }
} }
@ -305,6 +307,7 @@ LPSolver::SubProblem& LPSolver::unseal(size_t _problemIndex)
problem = make_shared<SubProblem>(*problem); problem = make_shared<SubProblem>(*problem);
problem->sealed = false; problem->sealed = false;
problem->result = nullopt; problem->result = nullopt;
problem->reasons.clear();
return *problem; return *problem;
} }
@ -345,7 +348,6 @@ void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom)
combineInto.basicVariables.emplace(index + varShift, row + rowShift); combineInto.basicVariables.emplace(index + varShift, row + rowShift);
for (auto&& [outerIndex, innerIndex]: combineFrom.varMapping) for (auto&& [outerIndex, innerIndex]: combineFrom.varMapping)
combineInto.varMapping.emplace(outerIndex, innerIndex + varShift); combineInto.varMapping.emplace(outerIndex, innerIndex + varShift);
combineInto.reasons += combineFrom.reasons;
for (auto& item: m_subProblemsPerVariable) for (auto& item: m_subProblemsPerVariable)
if (item.second == _combineFrom) if (item.second == _combineFrom)
@ -375,8 +377,6 @@ void LPSolver::addConstraintToSubProblem(
// together with the var. // together with the var.
SubProblem& problem = unseal(_subProblem); SubProblem& problem = unseal(_subProblem);
if (_reason)
problem.reasons.insert(*_reason);
size_t numVariables = 0; size_t numVariables = 0;
size_t latestVariableIndex = size_t(-1); size_t latestVariableIndex = size_t(-1);
@ -400,9 +400,9 @@ void LPSolver::addConstraintToSubProblem(
bound -= RationalWithDelta::delta(); bound -= RationalWithDelta::delta();
bound /= factor; bound /= factor;
if (factor > 0 || _constraint.kind == Constraint::EQUAL) if (factor > 0 || _constraint.kind == Constraint::EQUAL)
addUpperBound(latestVariableIndex, bound); addUpperBound(latestVariableIndex, bound, move(_reason));
if (factor < 0 || _constraint.kind == Constraint::EQUAL) if (factor < 0 || _constraint.kind == Constraint::EQUAL)
addLowerBound(latestVariableIndex, bound); addLowerBound(latestVariableIndex, bound, move(_reason));
return; return;
} }
@ -412,8 +412,12 @@ void LPSolver::addConstraintToSubProblem(
//problem.variables[slackIndex].name = "_s" + to_string(m_slackVariableCounter++); //problem.variables[slackIndex].name = "_s" + to_string(m_slackVariableCounter++);
problem.basicVariables[slackIndex] = problem.factors.size(); problem.basicVariables[slackIndex] = problem.factors.size();
if (_constraint.kind == Constraint::EQUAL) if (_constraint.kind == Constraint::EQUAL)
{
problem.variables[slackIndex].bounds.lower = _constraint.data[0]; problem.variables[slackIndex].bounds.lower = _constraint.data[0];
problem.variables[slackIndex].bounds.lowerReason = _reason;
}
problem.variables[slackIndex].bounds.upper = _constraint.data[0]; problem.variables[slackIndex].bounds.upper = _constraint.data[0];
problem.variables[slackIndex].bounds.upperReason = _reason;
if (_constraint.kind == Constraint::LESS_THAN) if (_constraint.kind == Constraint::LESS_THAN)
*problem.variables[slackIndex].bounds.upper -= RationalWithDelta::delta(); *problem.variables[slackIndex].bounds.upper -= RationalWithDelta::delta();
// TODO it is a basic var, so we don't add it, unless we use this for basic vars. // TODO it is a basic var, so we don't add it, unless we use this for basic vars.
@ -511,8 +515,11 @@ LPResult LPSolver::SubProblem::check()
pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar); pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar);
} }
else else
{
reasons = reasonsForUnsat(*bvi, true);
return LPResult::Infeasible; return LPResult::Infeasible;
} }
}
else if (basicVar.bounds.upper && basicVar.value > *basicVar.bounds.upper) else if (basicVar.bounds.upper && basicVar.value > *basicVar.bounds.upper)
{ {
if (auto replacementVar = firstReplacementVar(*bvi, false)) if (auto replacementVar = firstReplacementVar(*bvi, false))
@ -523,8 +530,11 @@ LPResult LPSolver::SubProblem::check()
pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar); pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar);
} }
else else
{
reasons = reasonsForUnsat(*bvi, false);
return LPResult::Infeasible; return LPResult::Infeasible;
} }
}
#ifdef DEBUG #ifdef DEBUG
cerr << "Fixed basic " << basicVar.name << endl; cerr << "Fixed basic " << basicVar.name << endl;
cerr << toString() << endl; cerr << toString() << endl;
@ -594,7 +604,14 @@ bool LPSolver::SubProblem::correctNonbasic()
{ {
Variable& var = variables.at(i); Variable& var = variables.at(i);
if (var.bounds.lower && var.bounds.upper && *var.bounds.lower > *var.bounds.upper) if (var.bounds.lower && var.bounds.upper && *var.bounds.lower > *var.bounds.upper)
{
reasons.clear();
if (var.bounds.lowerReason)
reasons.insert(*var.bounds.lowerReason);
if (var.bounds.upperReason)
reasons.insert(*var.bounds.upperReason);
return false; return false;
}
if (basicVariables.count(i)) if (basicVariables.count(i))
{ {
variablesPotentiallyOutOfBounds.insert(i); variablesPotentiallyOutOfBounds.insert(i);
@ -660,6 +677,34 @@ optional<size_t> LPSolver::SubProblem::firstReplacementVar(
return nullopt; return nullopt;
} }
set<size_t> LPSolver::SubProblem::reasonsForUnsat(
size_t _basicVarToReplace,
bool _increasing
) const
{
set<size_t> r;
if (_increasing && variables[_basicVarToReplace].bounds.lowerReason)
r.insert(*variables[_basicVarToReplace].bounds.lowerReason);
else if (!_increasing && variables[_basicVarToReplace].bounds.upperReason)
r.insert(*variables[_basicVarToReplace].bounds.upperReason);
LinearExpression const& basicVarEquation = factors[basicVariables.at(_basicVarToReplace)];
for (auto const& [i, factor]: basicVarEquation.enumerate())
{
if (i == _basicVarToReplace || !factor)
continue;
bool positive = factor > 0;
if (!_increasing)
positive = !positive;
Variable const& candidate = variables.at(i);
if (positive && candidate.bounds.upperReason)
r.insert(*candidate.bounds.upperReason);
if (!positive && candidate.bounds.lowerReason)
r.insert(*candidate.bounds.lowerReason);
}
return r;
}
void LPSolver::SubProblem::pivot(size_t _old, size_t _new) void LPSolver::SubProblem::pivot(size_t _old, size_t _new)
{ {
// Transform pivotRow such that the coefficient for _new is -1 // Transform pivotRow such that the coefficient for _new is -1

8
libsolutil/LP.h
View File

@ -295,8 +295,8 @@ class LPSolver
public: public:
void addConstraint(Constraint const& _constraint, std::optional<size_t> _reason = std::nullopt); void addConstraint(Constraint const& _constraint, std::optional<size_t> _reason = std::nullopt);
void setVariableName(size_t _variable, std::string _name); void setVariableName(size_t _variable, std::string _name);
void addLowerBound(size_t _variable, RationalWithDelta _bound); void addLowerBound(size_t _variable, RationalWithDelta _bound, std::optional<size_t> _reason = std::nullopt);
void addUpperBound(size_t _variable, RationalWithDelta _bound); void addUpperBound(size_t _variable, RationalWithDelta _bound, std::optional<size_t> _reason = std::nullopt);
std::pair<LPResult, ReasonSet>check(); std::pair<LPResult, ReasonSet>check();
@ -308,6 +308,8 @@ private:
{ {
std::optional<RationalWithDelta> lower; std::optional<RationalWithDelta> lower;
std::optional<RationalWithDelta> upper; std::optional<RationalWithDelta> upper;
std::optional<size_t> lowerReason;
std::optional<size_t> upperReason;
}; };
struct Variable struct Variable
{ {
@ -338,6 +340,8 @@ private:
/// @returns the index of the first basic variable violating its bounds. /// @returns the index of the first basic variable violating its bounds.
std::optional<size_t> firstConflictingBasicVariable() const; std::optional<size_t> firstConflictingBasicVariable() const;
std::optional<size_t> firstReplacementVar(size_t _basicVarToReplace, bool _increasing) const; std::optional<size_t> firstReplacementVar(size_t _basicVarToReplace, bool _increasing) const;
/// @returns the set of reasons in case "firstReplacementVar" failed.
std::set<size_t> reasonsForUnsat(size_t _basicVarToReplace, bool _increasing) const;
void pivot(size_t _old, size_t _new); void pivot(size_t _old, size_t _new);
void pivotAndUpdate(size_t _oldBasicVar, RationalWithDelta const& _newValue, size_t _newBasicVar); void pivotAndUpdate(size_t _oldBasicVar, RationalWithDelta const& _newValue, size_t _newBasicVar);