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

Multi-argument and and or.

Browse Source
This commit is contained in:
chriseth 2022-05-10 08:58:41 +02:00
parent f940e1f9e7
commit 91f32a7beb
1 changed files with 9 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
libsolutil/BooleanLP.cpp
View File

@ -113,6 +113,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
}
else if (_expr.name == "=")
{
solAssert(_expr.arguments.size() == 2);
solAssert(_expr.arguments.at(0).sort->kind == _expr.arguments.at(1).sort->kind);
if (_expr.arguments.at(0).sort->kind == Kind::Bool)
{
@ -150,28 +151,19 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
solAssert(false);
}
else if (_expr.name == "and")
{
addAssertion(_expr.arguments.at(0));
addAssertion(_expr.arguments.at(1));
}
for (auto const& arg: _expr.arguments)
addAssertion(arg);
else if (_expr.name == "or")
{
// We could try to parse a full clause here.
Literal left = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0));
Literal right = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(1));
/*
if (isConditionalConstraint(left.variable) && isConditionalConstraint(right.variable))
{
// We cannot have more than one constraint per clause.
// TODO Why?
right = *parseLiteral(declareInternalVariable(true));
addBooleanEquality(right, _expr.arguments.at(1));
}
*/
state().clauses.emplace_back(Clause{vector<Literal>{left, right}});
vector<Literal> literals;
// We could try to parse a full clause here instead.
for (auto const& arg: _expr.arguments)
literals.emplace_back(parseLiteralOrReturnEqualBoolean(arg));
state().clauses.emplace_back(Clause{move(literals)});
}
else if (_expr.name == "not")
{
solAssert(_expr.arguments.size() == 1);
// TODO can we still try to add a fixed constraint?
Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));
state().clauses.emplace_back(Clause{vector<Literal>{l}});