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

Fix interior multi-or and multi-and.

Browse Source
This commit is contained in:
chriseth 2022-05-31 14:21:13 +02:00
parent 02c6298ab8
commit 57c6c529d0
1 changed files with 20 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
libsolutil/BooleanLP.cpp
View File

@ -311,6 +311,10 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, LetBindings _letBind
for (auto const& arg: _expr.arguments) for (auto const& arg: _expr.arguments)
addAssertion(arg, _letBindings); addAssertion(arg, _letBindings);
else if (_expr.name == "or") else if (_expr.name == "or")
{
if (_expr.arguments.size() == 1)
addAssertion(_expr.arguments.front());
else
{ {
vector<Literal> literals; vector<Literal> literals;
// We could try to parse a full clause here instead. // We could try to parse a full clause here instead.
@ -318,6 +322,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, LetBindings _letBind
literals.emplace_back(parseLiteralOrReturnEqualBoolean(arg, _letBindings)); literals.emplace_back(parseLiteralOrReturnEqualBoolean(arg, _letBindings));
state().clauses.emplace_back(Clause{move(literals)}); state().clauses.emplace_back(Clause{move(literals)});
} }
}
else if (_expr.name == "xor") else if (_expr.name == "xor")
{ {
solAssert(_expr.arguments.size() == 2); solAssert(_expr.arguments.size() == 2);
@ -748,15 +753,17 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi
else else
{ {
Literal a = parseLiteralOrReturnEqualBoolean(_right.arguments.at(0), _letBindings); Literal a = parseLiteralOrReturnEqualBoolean(_right.arguments.at(0), _letBindings);
Literal b = parseLiteralOrReturnEqualBoolean(_right.arguments.at(1), _letBindings); Literal b;
/* if (_right.arguments.size() > 2)
if (isConditionalConstraint(a.variable) && isConditionalConstraint(b.variable))
{ {
// We cannot have more than one constraint per clause. solAssert(_right.name == "and" || _right.name == "or");
// TODO Why? // Reduce "a and b and c and ..." to "a and (b and c and ...)"
b = *parseLiteral(declareInternalVariable(true)); smtutil::Expression rightSuffix = _right;
addBooleanEquality(b, _right.arguments.at(1)); rightSuffix.arguments.erase(rightSuffix.arguments.begin());
}*/ b = parseLiteralOrReturnEqualBoolean(rightSuffix, _letBindings);
}
else
b = parseLiteralOrReturnEqualBoolean(_right.arguments.at(1), _letBindings);
if (_right.name == "and") if (_right.name == "and")
{ {