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

strict inequalities

Browse Source
This commit is contained in:
chriseth 2022-05-12 16:10:06 +02:00
parent 7b0e02b1ff
commit 657a02771b
10 changed files with 224 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsmtutil/SMTLib2Interface.cpp
View File

@ -219,6 +219,8 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
{ {
case Kind::Int: case Kind::Int:
return "Int"; return "Int";
case Kind::Real:
return "Real";
case Kind::Bool: case Kind::Bool:
return "Bool"; return "Bool";
case Kind::BitVector: case Kind::BitVector:
@ -278,8 +280,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{ {
auto const& e = _expressionsToEvaluate.at(i); auto const& e = _expressionsToEvaluate.at(i);
smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate."); smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool || e.sort->kind == Kind::Real, "Invalid sort for expression to evaluate.");
command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n"; command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + toSmtLibSort(*e.sort) + ")\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
} }
command += "(check-sat)\n"; command += "(check-sat)\n";

1
libsmtutil/Sorts.cpp
View File

@ -25,6 +25,7 @@ namespace solidity::smtutil
{ {
shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)}; shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};
shared_ptr<Sort> const SortProvider::realSort{make_shared<Sort>(Kind::Real)};
shared_ptr<IntSort> const SortProvider::uintSort{make_shared<IntSort>(false)}; shared_ptr<IntSort> const SortProvider::uintSort{make_shared<IntSort>(false)};
shared_ptr<IntSort> const SortProvider::sintSort{make_shared<IntSort>(true)}; shared_ptr<IntSort> const SortProvider::sintSort{make_shared<IntSort>(true)};

2
libsmtutil/Sorts.h
View File

@ -31,6 +31,7 @@ namespace solidity::smtutil
enum class Kind enum class Kind
{ {
Int, Int,
Real,
Bool, Bool,
BitVector, BitVector,
Function, Function,
@ -206,6 +207,7 @@ struct SortProvider
static std::shared_ptr<IntSort> const sintSort; static std::shared_ptr<IntSort> const sintSort;
static std::shared_ptr<IntSort> intSort(bool _signed = false); static std::shared_ptr<IntSort> intSort(bool _signed = false);
static std::shared_ptr<BitVectorSort> const bitVectorSort; static std::shared_ptr<BitVectorSort> const bitVectorSort;
static std::shared_ptr<Sort> const realSort;
}; };
} }

105
libsolutil/BooleanLP.cpp
View File

@ -92,10 +92,9 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s
{ {
// Internal variables are '$<number>', or '$c<number>' so escape `$` to `$$`. // Internal variables are '$<number>', or '$c<number>' so escape `$` to `$$`.
string name = (_name.empty() || _name.at(0) != '$') ? _name : "$$" + _name; string name = (_name.empty() || _name.at(0) != '$') ? _name : "$$" + _name;
// TODO This will not be an integer variable in our model. solAssert(_sort && (_sort->kind == Kind::Int || _sort->kind == Kind::Real || _sort->kind == Kind::Bool), "");
// Introduce a new kind?
solAssert(_sort && (_sort->kind == Kind::Int || _sort->kind == Kind::Bool), "");
solAssert(!state().variables.count(name), ""); solAssert(!state().variables.count(name), "");
// TODO store the actual kind (integer, real, bool)
declareVariable(name, _sort->kind == Kind::Bool); declareVariable(name, _sort->kind == Kind::Bool);
} }
@ -206,10 +205,10 @@ string BooleanLPSolver::toString() const
if (!bounds.lower && !bounds.upper) if (!bounds.lower && !bounds.upper)
continue; continue;
if (bounds.lower) if (bounds.lower)
result += ::toString(*bounds.lower) + " <= "; result += bounds.lower->toString() + " <= ";
result += variableName(index); result += variableName(index);
if (bounds.upper) if (bounds.upper)
result += " <= " + ::toString(*bounds.upper); result += " <= " + bounds.upper->toString();
result += "\n"; result += "\n";
} }
result += "-- Clauses:\n"; result += "-- Clauses:\n";
@ -251,7 +250,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
addBooleanEquality(newBoolean, _expr.arguments.at(1), _letBindings); addBooleanEquality(newBoolean, _expr.arguments.at(1), _letBindings);
} }
} }
else if (_expr.arguments.at(0).sort->kind == Kind::Int) else if (_expr.arguments.at(0).sort->kind == Kind::Int || _expr.arguments.at(0).sort->kind == Kind::Real)
{ {
// Try to see if both sides are linear. // Try to see if both sides are linear.
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings); optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
@ -260,7 +259,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
{ {
LinearExpression data = *left - *right; LinearExpression data = *left - *right;
data[0] *= -1; data[0] *= -1;
Constraint c{move(data), _expr.name == "="}; Constraint c{move(data), Constraint::EQUAL};
if (!tryAddDirectBounds(c)) if (!tryAddDirectBounds(c))
state().fixedConstraints.emplace_back(move(c)); state().fixedConstraints.emplace_back(move(c));
cerr << "Added as fixed constraint" << endl; cerr << "Added as fixed constraint" << endl;
@ -293,24 +292,20 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
} }
else if (_expr.name == "=>") else if (_expr.name == "=>")
addAssertion(!_expr.arguments.at(0) || _expr.arguments.at(1), move(_letBindings)); addAssertion(!_expr.arguments.at(0) || _expr.arguments.at(1), move(_letBindings));
else if (_expr.name == "<=") else if (_expr.name == "<=" || _expr.name == "<")
{ {
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings); optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1), _letBindings); optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1), _letBindings);
solAssert(left && right); solAssert(left && right);
LinearExpression data = *left - *right; LinearExpression data = *left - *right;
data[0] *= -1; data[0] *= -1;
Constraint c{move(data), _expr.name == "="}; // TODO if the type is integer, transform x < y into x <= y - 1
Constraint c{move(data), _expr.name == "<=" ? Constraint::LESS_OR_EQUAL : Constraint::LESS_THAN};
if (!tryAddDirectBounds(c)) if (!tryAddDirectBounds(c))
state().fixedConstraints.emplace_back(move(c)); state().fixedConstraints.emplace_back(move(c));
} }
else if (_expr.name == ">=") else if (_expr.name == ">=")
addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings)); addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings));
else if (_expr.name == "<")
{
cerr << "ERROR cannot properly encode '<'" << endl;
addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings));
}
else if (_expr.name == ">") else if (_expr.name == ">")
addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings)); addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings));
else else
@ -325,7 +320,8 @@ Expression BooleanLPSolver::declareInternalVariable(bool _boolean)
{ {
string name = "$" + to_string(state().variables.size() + 1); string name = "$" + to_string(state().variables.size() + 1);
declareVariable(name, _boolean); declareVariable(name, _boolean);
return smtutil::Expression(name, {}, _boolean ? SortProvider::boolSort : SortProvider::uintSort); // TODO also support integer
return smtutil::Expression(name, {}, _boolean ? SortProvider::boolSort : SortProvider::realSort);
} }
void BooleanLPSolver::declareVariable(string const& _name, bool _boolean) void BooleanLPSolver::declareVariable(string const& _name, bool _boolean)
@ -369,27 +365,25 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
} }
else if (_expr.name == "not") else if (_expr.name == "not")
return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0), move(_letBindings))); return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0), move(_letBindings)));
else if (_expr.name == "<=" || _expr.name == "=") else if (_expr.name == "<=" || _expr.name == "<" || _expr.name == "=")
{ {
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings); optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1), _letBindings); optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1), _letBindings);
if (!left || !right) if (!left || !right)
return {}; return {};
// TODO if the type is int, use x < y -> x <= y - 1
LinearExpression data = *left - *right; LinearExpression data = *left - *right;
data[0] *= -1; data[0] *= -1;
return Literal{true, addConditionalConstraint(Constraint{move(data), _expr.name == "="})}; Constraint::Kind kind =
_expr.name == "<=" ? Constraint::LESS_OR_EQUAL :
_expr.name == "<" ? Constraint::LESS_THAN :
Constraint::EQUAL;
return Literal{true, addConditionalConstraint(Constraint{move(data), kind})};
} }
else if (_expr.name == ">=") else if (_expr.name == ">=")
return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings)); return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings));
else if (_expr.name == "<")
{
cerr << "ERROR cannot properly encode '<'" << endl;
// TODO this is not the theory of reals!
return parseLiteral(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings));
}
else if (_expr.name == ">") else if (_expr.name == ">")
return parseLiteral(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings)); return parseLiteral(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings));
@ -401,12 +395,12 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
if (isConditionalConstraint(_lit.variable)) if (isConditionalConstraint(_lit.variable))
{ {
Constraint const& c = conditionalConstraint(_lit.variable); Constraint const& c = conditionalConstraint(_lit.variable);
if (c.equality) if (c.kind == Constraint::EQUAL)
{ {
// X = b // X = b
cerr << "ERROR cannot properly encode '<'" << endl;
/* This is the integer case
// X <= b - 1 // X <= b - 1
Constraint le = c; Constraint le = c;
le.equality = false; le.equality = false;
@ -421,24 +415,42 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
ge.data[0] -= 1; ge.data[0] -= 1;
Literal geL{true, addConditionalConstraint(ge)}; Literal geL{true, addConditionalConstraint(ge)};
*/
// X < b
Constraint lt = c;
lt.kind = Constraint::LESS_THAN;
Literal ltL{true, addConditionalConstraint(lt)};
// X > b <=> -X < -b
Constraint gt = c;
gt.kind = Constraint::LESS_THAN;
gt.data *= -1;
Literal gtL{true, addConditionalConstraint(gt)};
Literal equalBoolean = *parseLiteral(declareInternalVariable(true), {}); Literal equalBoolean = *parseLiteral(declareInternalVariable(true), {});
// a = or(x, y) <=> (-a \/ x \/ y) /\ (a \/ -x) /\ (a \/ -y) // a = or(x, y) <=> (-a \/ x \/ y) /\ (a \/ -x) /\ (a \/ -y)
state().clauses.emplace_back(Clause{vector<Literal>{negate(equalBoolean), leL, geL}}); state().clauses.emplace_back(Clause{vector<Literal>{negate(equalBoolean), ltL, gtL}});
state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(leL)}}); state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(ltL)}});
state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(geL)}}); state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(gtL)}});
return equalBoolean; return equalBoolean;
} }
else else
{ {
cerr << "ERROR cannot properly encode '<'" << endl; /* This is the integer case
// X > b
// -x < -b // -x < -b
// -x <= -b - 1 // -x <= -b - 1
Constraint negated = c; Constraint negated = c;
negated.data *= -1; negated.data *= -1;
negated.data[0] -= 1; negated.data[0] -= 1;
*/
// !(X <= b) <=> X > b <=> -X < -b
// !(X < b) <=> X >= b <=> -X <= -b
Constraint negated = c;
negated.data *= -1;
negated.kind = c.kind == Constraint::LESS_THAN ? Constraint::LESS_OR_EQUAL : Constraint::LESS_THAN;
return Literal{true, addConditionalConstraint(negated)}; return Literal{true, addConditionalConstraint(negated)};
} }
} }
@ -547,10 +559,11 @@ bool BooleanLPSolver::tryAddDirectBounds(Constraint const& _constraint)
//cerr << "adding direct bound." << endl; //cerr << "adding direct bound." << endl;
if (ranges::distance(nonzero) == 0) if (ranges::distance(nonzero) == 0)
{ {
// 0 <= b or 0 = b // 0 < b or 0 <= b or 0 = b
if ( if (
_constraint.data.front() < 0 || (_constraint.kind == Constraint::LESS_THAN && _constraint.data.front() <= 0) ||
(_constraint.equality && _constraint.data.front() != 0) (_constraint.kind == Constraint::LESS_OR_EQUAL && _constraint.data.front() < 0) ||
(_constraint.kind == Constraint::EQUAL && _constraint.data.front() != 0)
) )
{ {
// cerr << "SETTING INF" << endl; // cerr << "SETTING INF" << endl;
@ -560,27 +573,29 @@ bool BooleanLPSolver::tryAddDirectBounds(Constraint const& _constraint)
else else
{ {
auto&& [varIndex, factor] = nonzero.front(); auto&& [varIndex, factor] = nonzero.front();
// a * x <= b // a * x <= b or a * x < b or a * x = b
rational bound = _constraint.data[0] / factor;
if (factor > 0 || _constraint.equality) RationalWithDelta bound = _constraint.data[0];
if (_constraint.kind == Constraint::LESS_THAN)
bound -= RationalWithDelta::delta();
bound /= factor;
if (factor > 0 || _constraint.kind == Constraint::EQUAL)
addUpperBound(varIndex, bound); addUpperBound(varIndex, bound);
if (factor < 0 || _constraint.equality) if (factor < 0 || _constraint.kind == Constraint::EQUAL)
addLowerBound(varIndex, bound); addLowerBound(varIndex, bound);
} }
return true; return true;
} }
void BooleanLPSolver::addUpperBound(size_t _index, rational _value) void BooleanLPSolver::addUpperBound(size_t _index, RationalWithDelta _value)
{ {
//cerr << "adding " << variableName(_index) << " <= " << toString(_value) << endl; //cerr << "adding " << variableName(_index) << " <= " << toString(_value) << endl;
if (!state().bounds[_index].upper || _value < *state().bounds[_index].upper) if (!state().bounds[_index].upper || _value < *state().bounds[_index].upper)
state().bounds[_index].upper = move(_value); state().bounds[_index].upper = move(_value);
} }
void BooleanLPSolver::addLowerBound(size_t _index, rational _value) void BooleanLPSolver::addLowerBound(size_t _index, RationalWithDelta _value)
{ {
// Lower bound must be at least zero.
_value = max(_value, rational{});
//cerr << "adding " << variableName(_index) << " >= " << toString(_value) << endl; //cerr << "adding " << variableName(_index) << " >= " << toString(_value) << endl;
if (!state().bounds[_index].lower || _value > *state().bounds[_index].lower) if (!state().bounds[_index].lower || _value > *state().bounds[_index].lower)
state().bounds[_index].lower = move(_value); state().bounds[_index].lower = move(_value);
@ -712,7 +727,11 @@ string BooleanLPSolver::toString(Constraint const& _constraint) const
// TODO reasons? // TODO reasons?
return return
joinHumanReadable(line, " + ") + joinHumanReadable(line, " + ") +
(_constraint.equality ? " = " : " <= ") + (
_constraint.kind == Constraint::EQUAL ? " = " :
_constraint.kind == Constraint::LESS_OR_EQUAL ? " <= " :
" < "
) +
::toString(_constraint.data.front()); ::toString(_constraint.data.front());
} }

8
libsolutil/BooleanLP.h
View File

@ -42,8 +42,8 @@ struct State
struct Bounds struct Bounds
{ {
std::optional<rational> lower; std::optional<RationalWithDelta> lower;
std::optional<rational> upper; std::optional<RationalWithDelta> upper;
}; };
// Unconditional bounds on variables // Unconditional bounds on variables
@ -115,8 +115,8 @@ private:
std::optional<LinearExpression> parseFactor(smtutil::Expression const& _expression, std::map<std::string, size_t> _letBindings) const; std::optional<LinearExpression> parseFactor(smtutil::Expression const& _expression, std::map<std::string, size_t> _letBindings) const;
bool tryAddDirectBounds(Constraint const& _constraint); bool tryAddDirectBounds(Constraint const& _constraint);
void addUpperBound(size_t _index, rational _value); void addUpperBound(size_t _index, RationalWithDelta _value);
void addLowerBound(size_t _index, rational _value); void addLowerBound(size_t _index, RationalWithDelta _value);
size_t addConditionalConstraint(Constraint _constraint); size_t addConditionalConstraint(Constraint _constraint);

68
libsolutil/LP.cpp
View File

@ -86,11 +86,10 @@ string reasonToString(ReasonSet const& _reasons, size_t _minSize)
} }
bool Constraint::operator<(Constraint const& _other) const bool Constraint::operator<(Constraint const& _other) const
{ {
if (equality != _other.equality) if (kind != _other.kind)
return equality < _other.equality; return kind < _other.kind;
for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i)
if (rational diff = data.get(i) - _other.data.get(i)) if (rational diff = data.get(i) - _other.data.get(i))
@ -105,7 +104,7 @@ bool Constraint::operator<(Constraint const& _other) const
bool Constraint::operator==(Constraint const& _other) const bool Constraint::operator==(Constraint const& _other) const
{ {
if (equality != _other.equality) if (kind != _other.kind)
return false; return false;
for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i)
@ -119,6 +118,17 @@ bool Constraint::operator==(Constraint const& _other) const
return true; return true;
} }
string RationalWithDelta::toString() const
{
string result = ::toString(m_main);
if (m_delta)
result +=
(m_delta > 0 ? "+" : "-") +
(abs(m_delta) == 1 ? "" : ::toString(abs(m_delta))) +
"d";
return result;
}
bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const
{ {
if (!considerVariableNames || _a.variableNames == _b.variableNames) if (!considerVariableNames || _a.variableNames == _b.variableNames)
@ -160,7 +170,11 @@ string SolvingState::toString() const
} }
result += result +=
joinHumanReadable(line, " + ") + joinHumanReadable(line, " + ") +
(constraint.equality ? " = " : " <= ") + (
constraint.kind == Constraint::EQUAL ? " = " :
constraint.kind == Constraint::LESS_OR_EQUAL ? " <= " :
" < "
) +
::toString(constraint.data.front()) + ::toString(constraint.data.front()) +
"\n"; "\n";
} }
@ -172,10 +186,10 @@ string SolvingState::toString() const
if (bounds.lower) if (bounds.lower)
result += result +=
reasonToString(bounds.lowerReasons, reasonLength) + reasonToString(bounds.lowerReasons, reasonLength) +
::toString(*bounds.lower) + " <= "; bounds.lower->toString() + " <= ";
result += variableNames.at(index); result += variableNames.at(index);
if (bounds.upper) if (bounds.upper)
result += " <= "s + ::toString(*bounds.upper) + " " + reasonToString(bounds.upperReasons, 0); result += " <= "s + bounds.upper->toString() + " " + reasonToString(bounds.upperReasons, 0);
result += "\n"; result += "\n";
} }
return result; return result;
@ -215,7 +229,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, rational _bound) void LPSolver::addLowerBound(size_t _variable, RationalWithDelta _bound)
{ {
SubProblem& p = unsealForVariable(_variable); SubProblem& p = unsealForVariable(_variable);
size_t innerIndex = p.varMapping.at(_variable); size_t innerIndex = p.varMapping.at(_variable);
@ -227,7 +241,7 @@ void LPSolver::addLowerBound(size_t _variable, rational _bound)
} }
} }
void LPSolver::addUpperBound(size_t _variable, rational _bound) void LPSolver::addUpperBound(size_t _variable, RationalWithDelta _bound)
{ {
SubProblem& p = unsealForVariable(_variable); SubProblem& p = unsealForVariable(_variable);
size_t innerIndex = p.varMapping.at(_variable); size_t innerIndex = p.varMapping.at(_variable);
@ -274,7 +288,10 @@ map<string, rational> LPSolver::model() const
for (auto const& problem: m_subProblems) for (auto const& problem: m_subProblems)
if (problem) if (problem)
for (auto&& [outerIndex, innerIndex]: problem->varMapping) for (auto&& [outerIndex, innerIndex]: problem->varMapping)
result[problem->variables[innerIndex].name] = problem->variables[innerIndex].value; // TODO assign proper value to "delta"
result[problem->variables[innerIndex].name] =
problem->variables[innerIndex].value.m_main +
problem->variables[innerIndex].value.m_delta / rational(100000);
return result; return result;
} }
@ -376,10 +393,13 @@ void LPSolver::addConstraintToSubProblem(
// TODO we could avoid some of the steps by introducing an "addUpperBound" // TODO we could avoid some of the steps by introducing an "addUpperBound"
// function on the subproblem. // function on the subproblem.
rational factor = _constraint.data[latestVariableIndex]; rational factor = _constraint.data[latestVariableIndex];
rational bound = _constraint.data.front() / factor; RationalWithDelta bound = _constraint.data.front();
if (factor > 0 || _constraint.equality) if (_constraint.kind == Constraint::LESS_THAN)
bound -= RationalWithDelta::delta();
bound /= factor;
if (factor > 0 || _constraint.kind == Constraint::EQUAL)
addUpperBound(latestVariableIndex, bound); addUpperBound(latestVariableIndex, bound);
if (factor < 0 || _constraint.equality) if (factor < 0 || _constraint.kind == Constraint::EQUAL)
addLowerBound(latestVariableIndex, bound); addLowerBound(latestVariableIndex, bound);
return; return;
} }
@ -389,15 +409,17 @@ void LPSolver::addConstraintToSubProblem(
// Name is only needed for printing // Name is only needed for printing
//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.equality) 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.upper = _constraint.data[0]; problem.variables[slackIndex].bounds.upper = _constraint.data[0];
if (_constraint.kind == Constraint::LESS_THAN)
*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.
//problem.variablesPotentiallyOutOfBounds.insert(slackIndex); //problem.variablesPotentiallyOutOfBounds.insert(slackIndex);
// Compress the constraint, i.e. turn outer variable indices into // Compress the constraint, i.e. turn outer variable indices into
// inner variable indices. // inner variable indices.
rational valueForSlack; RationalWithDelta valueForSlack;
LinearExpression compressedConstraint; LinearExpression compressedConstraint;
LinearExpression basicVarNullifier; LinearExpression basicVarNullifier;
compressedConstraint.resize(problem.variables.size()); compressedConstraint.resize(problem.variables.size());
@ -504,15 +526,15 @@ string LPSolver::SubProblem::toString() const
for (auto&& [i, v]: variables | ranges::views::enumerate) for (auto&& [i, v]: variables | ranges::views::enumerate)
{ {
if (v.bounds.lower) if (v.bounds.lower)
resultString += ::toString(*v.bounds.lower) + " <= "; resultString += v.bounds.lower->toString() + " <= ";
else else
resultString += " "; resultString += " ";
resultString += v.name; resultString += v.name;
if (v.bounds.upper) if (v.bounds.upper)
resultString += " <= " + ::toString(*v.bounds.upper); resultString += " <= " + v.bounds.upper->toString();
else else
resultString += " "; resultString += " ";
resultString += " := " + ::toString(v.value) + "\n"; resultString += " := " + v.value.toString() + "\n";
} }
for (auto&& [rowIndex, row]: factors | ranges::views::enumerate) for (auto&& [rowIndex, row]: factors | ranges::views::enumerate)
{ {
@ -574,9 +596,9 @@ bool LPSolver::SubProblem::correctNonbasic()
return true; return true;
} }
void LPSolver::SubProblem::update(size_t _varIndex, rational const& _value) void LPSolver::SubProblem::update(size_t _varIndex, RationalWithDelta const& _value)
{ {
rational delta = _value - variables[_varIndex].value; RationalWithDelta delta = _value - variables[_varIndex].value;
variables[_varIndex].value = _value; variables[_varIndex].value = _value;
for (size_t j = 0; j < variables.size(); j++) for (size_t j = 0; j < variables.size(); j++)
if (basicVariables.count(j) && factors[basicVariables.at(j)][_varIndex]) if (basicVariables.count(j) && factors[basicVariables.at(j)][_varIndex])
@ -658,18 +680,18 @@ void LPSolver::SubProblem::pivot(size_t _old, size_t _new)
void LPSolver::SubProblem::pivotAndUpdate( void LPSolver::SubProblem::pivotAndUpdate(
size_t _oldBasicVar, size_t _oldBasicVar,
rational const& _newValue, RationalWithDelta const& _newValue,
size_t _newBasicVar size_t _newBasicVar
) )
{ {
rational theta = (_newValue - variables[_oldBasicVar].value) / factors[basicVariables[_oldBasicVar]][_newBasicVar]; RationalWithDelta theta = (_newValue - variables[_oldBasicVar].value) / factors[basicVariables[_oldBasicVar]][_newBasicVar];
variables[_oldBasicVar].value = _newValue; variables[_oldBasicVar].value = _newValue;
variables[_newBasicVar].value += theta; variables[_newBasicVar].value += theta;
for (auto const& [i, row]: basicVariables) for (auto const& [i, row]: basicVariables)
if (i != _oldBasicVar && factors[row][_newBasicVar]) if (i != _oldBasicVar && factors[row][_newBasicVar])
variables[i].value += factors[row][_newBasicVar] * theta; variables[i].value += theta * factors[row][_newBasicVar];
pivot(_oldBasicVar, _newBasicVar); pivot(_oldBasicVar, _newBasicVar);
} }

94
libsolutil/LP.h
View File

@ -34,14 +34,16 @@ using ReasonSet = std::set<size_t>;
/** /**
* Constraint of the form * Constraint of the form
* - data[1] * x_1 + data[2] * x_2 + ... <= data[0] (equality == false) * - data[1] * x_1 + data[2] * x_2 + ... <= data[0] (LESS_OR_EQUAL)
* - data[1] * x_1 + data[2] * x_2 + ... = data[0] (equality == true) * - data[1] * x_1 + data[2] * x_2 + ... < data[0] (LESS_THAN)
* - data[1] * x_1 + data[2] * x_2 + ... = data[0] (EQUAL)
* The set and order of variables is implied. * The set and order of variables is implied.
*/ */
struct Constraint struct Constraint
{ {
LinearExpression data; LinearExpression data;
bool equality = false; enum Kind { EQUAL, LESS_THAN, LESS_OR_EQUAL };
Kind kind = LESS_OR_EQUAL;
bool operator<(Constraint const& _other) const; bool operator<(Constraint const& _other) const;
bool operator==(Constraint const& _other) const; bool operator==(Constraint const& _other) const;
@ -52,10 +54,9 @@ struct Constraint
* x > 0 is transformed into x >= 1*delta, where delta is assumed to be "small". Its value * x > 0 is transformed into x >= 1*delta, where delta is assumed to be "small". Its value
* is never explicitly computed / set, it is just a symbolic parameter. * is never explicitly computed / set, it is just a symbolic parameter.
*/ */
class RationalWithDelta struct RationalWithDelta
{ {
public: RationalWithDelta(rational _x = {}): m_main(move(_x)) {}
RationalWithDelta(rational _x): m_main(move(_x)) {}
static RationalWithDelta delta() static RationalWithDelta delta()
{ {
RationalWithDelta x(0); RationalWithDelta x(0);
@ -69,30 +70,69 @@ public:
m_delta += _other.m_delta; m_delta += _other.m_delta;
return *this; return *this;
} }
RationalWithDelta& operator-=(RationalWithDelta const& _other)
{
m_main -= _other.m_main;
m_delta -= _other.m_delta;
return *this;
}
RationalWithDelta operator-(RationalWithDelta const& _other) const
{
RationalWithDelta ret = *this;
ret -= _other;
return ret;
}
RationalWithDelta& operator*=(rational const& _factor) RationalWithDelta& operator*=(rational const& _factor)
{ {
m_main *= _factor; m_main *= _factor;
m_delta *= _factor; m_delta *= _factor;
return *this; return *this;
} }
bool operator<=(RationalWithDelta const& _other) RationalWithDelta operator*(rational const& _factor) const
{
RationalWithDelta ret = *this;
ret *= _factor;
return ret;
}
RationalWithDelta& operator/=(rational const& _factor)
{
m_main /= _factor;
m_delta /= _factor;
return *this;
}
RationalWithDelta operator/(rational const& _factor) const
{
RationalWithDelta ret = *this;
ret /= _factor;
return ret;
}
bool operator<=(RationalWithDelta const& _other) const
{ {
return std::tie(m_main, m_delta) <= std::tie(_other.m_main, _other.m_delta); return std::tie(m_main, m_delta) <= std::tie(_other.m_main, _other.m_delta);
} }
bool operator<(RationalWithDelta const& _other) bool operator>=(RationalWithDelta const& _other) const
{
return std::tie(m_main, m_delta) >= std::tie(_other.m_main, _other.m_delta);
}
bool operator<(RationalWithDelta const& _other) const
{ {
return std::tie(m_main, m_delta) < std::tie(_other.m_main, _other.m_delta); return std::tie(m_main, m_delta) < std::tie(_other.m_main, _other.m_delta);
} }
bool operator==(RationalWithDelta const& _other) bool operator>(RationalWithDelta const& _other) const
{
return std::tie(m_main, m_delta) > std::tie(_other.m_main, _other.m_delta);
}
bool operator==(RationalWithDelta const& _other) const
{ {
return std::tie(m_main, m_delta) == std::tie(_other.m_main, _other.m_delta); return std::tie(m_main, m_delta) == std::tie(_other.m_main, _other.m_delta);
} }
bool operator!=(RationalWithDelta const& _other) bool operator!=(RationalWithDelta const& _other) const
{ {
return std::tie(m_main, m_delta) != std::tie(_other.m_main, _other.m_delta); return std::tie(m_main, m_delta) != std::tie(_other.m_main, _other.m_delta);
} }
private: std::string toString() const;
rational m_main; rational m_main;
rational m_delta; rational m_delta;
}; };
@ -107,8 +147,8 @@ struct SolvingState
std::vector<std::string> variableNames; std::vector<std::string> variableNames;
struct Bounds struct Bounds
{ {
std::optional<rational> lower; std::optional<RationalWithDelta> lower;
std::optional<rational> upper; std::optional<RationalWithDelta> upper;
bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); } bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); }
bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); } bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); }
@ -158,6 +198,18 @@ inline void hashCombineVector(std::size_t& _seed, std::vector<T> const& _v)
hashCombine(_seed, x); hashCombine(_seed, x);
} }
template<>
struct std::hash<solidity::util::RationalWithDelta>
{
std::size_t operator()(solidity::util::RationalWithDelta const& _x) const noexcept
{
std::size_t result = 0;
hashCombine(result, _x.m_main);
hashCombine(result, _x.m_delta);
return result;
}
};
template<> template<>
struct std::hash<solidity::util::SolvingState::Bounds> struct std::hash<solidity::util::SolvingState::Bounds>
{ {
@ -189,7 +241,7 @@ struct std::hash<solidity::util::Constraint>
std::size_t operator()(solidity::util::Constraint const& _constraint) const noexcept std::size_t operator()(solidity::util::Constraint const& _constraint) const noexcept
{ {
std::size_t result = 0; std::size_t result = 0;
hashCombine(result, _constraint.equality); hashCombine(result, _constraint.kind);
hashCombine(result, _constraint.data); hashCombine(result, _constraint.data);
return result; return result;
} }
@ -243,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, rational _bound); void addLowerBound(size_t _variable, RationalWithDelta _bound);
void addUpperBound(size_t _variable, rational _bound); void addUpperBound(size_t _variable, RationalWithDelta _bound);
std::pair<LPResult, ReasonSet>check(); std::pair<LPResult, ReasonSet>check();
@ -254,13 +306,13 @@ public:
private: private:
struct Bounds struct Bounds
{ {
std::optional<rational> lower; std::optional<RationalWithDelta> lower;
std::optional<rational> upper; std::optional<RationalWithDelta> upper;
}; };
struct Variable struct Variable
{ {
std::string name = {}; std::string name = {};
rational value = 0; RationalWithDelta value = {};
Bounds bounds = {}; Bounds bounds = {};
}; };
struct SubProblem struct SubProblem
@ -282,13 +334,13 @@ private:
private: private:
bool correctNonbasic(); bool correctNonbasic();
/// Set value of non-basic variable. /// Set value of non-basic variable.
void update(size_t _varIndex, rational const& _value); void update(size_t _varIndex, RationalWithDelta const& _value);
/// @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;
void pivot(size_t _old, size_t _new); void pivot(size_t _old, size_t _new);
void pivotAndUpdate(size_t _oldBasicVar, rational const& _newValue, size_t _newBasicVar); void pivotAndUpdate(size_t _oldBasicVar, RationalWithDelta const& _newValue, size_t _newBasicVar);
}; };

3
test/libsolutil/BooleanLP.cpp
View File

@ -196,6 +196,9 @@ BOOST_AUTO_TEST_CASE(splittable)
Expression w = variable("w"); Expression w = variable("w");
solver.addAssertion(x < y); solver.addAssertion(x < y);
solver.addAssertion(x < y - 2); solver.addAssertion(x < y - 2);
solver.addAssertion(x >= 0);
solver.addAssertion(y >= 0);
solver.addAssertion(w >= 0);
solver.addAssertion(z + w == 28); solver.addAssertion(z + w == 28);
solver.push(); solver.push();

30
test/libsolutil/LP.cpp
View File

@ -55,12 +55,25 @@ public:
{ {
_lhs -= _rhs; _lhs -= _rhs;
_lhs[0] = -_lhs[0]; _lhs[0] = -_lhs[0];
m_solver.addConstraint({move(_lhs), false}, move(_reason)); m_solver.addConstraint({move(_lhs), Constraint::LESS_OR_EQUAL}, move(_reason));
} }
void addLEConstraint(LinearExpression _lhs, rational _rhs) void addLEConstraint(LinearExpression _lhs, rational _rhs)
{ {
addLEConstraint(move(_lhs), constant(_rhs)); addLEConstraint(move(_lhs), LinearExpression::constant(move(_rhs)));
}
/// Adds the constraint "_lhs < _rhs".
void addLTConstraint(LinearExpression _lhs, LinearExpression _rhs, optional<size_t> _reason = {})
{
_lhs -= _rhs;
_lhs[0] = -_lhs[0];
m_solver.addConstraint({move(_lhs), Constraint::LESS_THAN}, move(_reason));
}
void addLTConstraint(LinearExpression _lhs, rational _rhs)
{
addLTConstraint(move(_lhs), LinearExpression::constant(move(_rhs)));
} }
/// Adds the constraint "_lhs = _rhs". /// Adds the constraint "_lhs = _rhs".
@ -68,7 +81,7 @@ public:
{ {
_lhs -= _rhs; _lhs -= _rhs;
_lhs[0] = -_lhs[0]; _lhs[0] = -_lhs[0];
m_solver.addConstraint({move(_lhs), true}, move(_reason)); m_solver.addConstraint({move(_lhs), Constraint::EQUAL}, move(_reason));
} }
void addLowerBound(string _variable, rational _value) void addLowerBound(string _variable, rational _value)
@ -425,6 +438,17 @@ BOOST_AUTO_TEST_CASE(reasons_joined)
infeasible({0, 2, 3}); infeasible({0, 2, 3});
} }
BOOST_AUTO_TEST_CASE(less_than)
{
auto x = variable("x");
addLTConstraint(2 * x, 10);
feasible({{"x", 0}});
addLowerBound("x", 4);
feasible({{"x", 4}});
addLowerBound("x", 5);
infeasible();
}
BOOST_AUTO_TEST_CASE(fuzzer2) BOOST_AUTO_TEST_CASE(fuzzer2)
{ {

7
tools/solsmt.cpp
View File

@ -143,7 +143,7 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<stri
return std::visit(GenericVisitor{ return std::visit(GenericVisitor{
[&](string_view const& _atom) { [&](string_view const& _atom) {
if (isDigit(_atom.front()) || _atom.front() == '.') if (isDigit(_atom.front()) || _atom.front() == '.')
return Expression(parseRational(_atom)); return Expression(parseRational(_atom).str(), {}, SortProvider::realSort);
else else
return Expression(string(_atom), {}, _variableSorts.at(string(_atom))); return Expression(string(_atom), {}, _variableSorts.at(string(_atom)));
}, },
@ -179,7 +179,7 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<stri
sort = sort =
contains(boolOperators, op) ? contains(boolOperators, op) ?
SortProvider::boolSort : SortProvider::boolSort :
SortProvider::intSort(); // TODO should be real at some point arguments.back().sort;
} }
return Expression(string(op), move(arguments), move(sort)); return Expression(string(op), move(arguments), move(sort));
} }
@ -245,8 +245,7 @@ int main(int argc, char** argv)
solAssert(get<vector<SMTLib2Expression>>(items[2].data).empty()); solAssert(get<vector<SMTLib2Expression>>(items[2].data).empty());
string_view type = get<string_view>(items[3].data); string_view type = get<string_view>(items[3].data);
solAssert(type == "Real" || type == "Bool"); solAssert(type == "Real" || type == "Bool");
// TODO should be real, but we call it int... SortPointer sort = type == "Real" ? SortProvider::realSort : SortProvider::boolSort;
SortPointer sort = type == "Real" ? SortProvider::intSort() : SortProvider::boolSort;
variableSorts[variableName] = sort; variableSorts[variableName] = sort;
solver.declareVariable(variableName, move(sort)); solver.declareVariable(variableName, move(sort));
} }