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

Remove "only single constraint" restriction.

Browse Source
This commit is contained in:
chriseth 2022-03-03 19:51:25 +01:00
parent fe15610ba4
commit 33f0e0d4b2
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolutil/BooleanLP.cpp
View File

@ -155,6 +155,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
// We could try to parse a full clause here. // We could try to parse a full clause here.
Literal left = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)); Literal left = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0));
Literal right = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(1)); Literal right = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(1));
/*
if (isConditionalConstraint(left.variable) && isConditionalConstraint(right.variable)) if (isConditionalConstraint(left.variable) && isConditionalConstraint(right.variable))
{ {
// We cannot have more than one constraint per clause. // We cannot have more than one constraint per clause.
@ -162,6 +163,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
right = *parseLiteral(declareInternalVariable(true)); right = *parseLiteral(declareInternalVariable(true));
addBooleanEquality(right, _expr.arguments.at(1)); addBooleanEquality(right, _expr.arguments.at(1));
} }
*/
state().clauses.emplace_back(Clause{vector<Literal>{left, right}}); state().clauses.emplace_back(Clause{vector<Literal>{left, right}});
} }
else if (_expr.name == "not") else if (_expr.name == "not")
@ -534,13 +536,14 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi
{ {
Literal a = parseLiteralOrReturnEqualBoolean(_right.arguments.at(0)); Literal a = parseLiteralOrReturnEqualBoolean(_right.arguments.at(0));
Literal b = parseLiteralOrReturnEqualBoolean(_right.arguments.at(1)); Literal b = parseLiteralOrReturnEqualBoolean(_right.arguments.at(1));
/*
if (isConditionalConstraint(a.variable) && isConditionalConstraint(b.variable)) if (isConditionalConstraint(a.variable) && isConditionalConstraint(b.variable))
{ {
// We cannot have more than one constraint per clause. // We cannot have more than one constraint per clause.
// TODO Why? // TODO Why?
b = *parseLiteral(declareInternalVariable(true)); b = *parseLiteral(declareInternalVariable(true));
addBooleanEquality(b, _right.arguments.at(1)); addBooleanEquality(b, _right.arguments.at(1));
} }*/
if (_right.name == "and") if (_right.name == "and")
{ {