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

Implement => for boolean equality.

Browse Source
This commit is contained in:
chriseth 2022-06-01 13:23:43 +02:00
parent 57c6c529d0
commit 9078ed8afd
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolutil/BooleanLP.cpp
View File

@ -779,6 +779,12 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi
state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a)}}); state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a)}});
state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(b)}}); state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(b)}});
} }
else if (_right.name == "=>")
{
solAssert(_right.arguments.size() == 2);
// a = (x => y) <=> a = or(-x, y)
addBooleanEquality(_left, !_right.arguments.at(0) || _right.arguments.at(1), move(_letBindings));
}
else if (_right.name == "=") else if (_right.name == "=")
{ {
// l = eq(a, b) <=> (-l or -a or b) and (-l or a or -b) and (l or -a or -b) and (l or a or b) // l = eq(a, b) <=> (-l or -a or b) and (-l or a or -b) and (l or -a or -b) and (l or a or b)