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

Add equality constraints.

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

51
libsolutil/BooleanLP.cpp
View File

@ -330,7 +330,7 @@ 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))); return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));
else if (_expr.name == "<=") else if (_expr.name == "<=" || _expr.name == "=")
{ {
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0)); optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0));
optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1)); optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1));
@ -340,7 +340,7 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
LinearExpression data = *left - *right; LinearExpression data = *left - *right;
data[0] *= -1; data[0] *= -1;
return Literal{true, addConditionalConstraint(Constraint{move(data), false, {}})}; return Literal{true, addConditionalConstraint(Constraint{move(data), _expr.name == "=", {}})};
} }
else if (_expr.name == ">=") else if (_expr.name == ">=")
return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0)); return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0));
@ -357,17 +357,46 @@ 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);
solAssert(!c.equality, ""); if (c.equality)
{
// X = b
// X > b // X <= b - 1
// -x < -b Constraint le = c;
// -x <= -b - 1 le.equality = false;
le.data[0] -= 1;
le.reasons.clear();
Literal leL{true, addConditionalConstraint(le)};
Constraint negated = c; // X >= b + 1
negated.data *= -1; // -X <= -b - 1
negated.data[0] -= 1; Constraint ge = c;
negated.reasons.clear(); ge.equality = false;
return Literal{true, addConditionalConstraint(negated)}; ge.data *= -1;
ge.data[0] -= 1;
ge.reasons.clear();
Literal geL{true, addConditionalConstraint(ge)};
Literal equalBoolean = *parseLiteral(declareInternalVariable(true));
// 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>{equalBoolean, negate(leL)}});
state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(geL)}});
return equalBoolean;
}
else
{
// X > b
// -x < -b
// -x <= -b - 1
Constraint negated = c;
negated.data *= -1;
negated.data[0] -= 1;
negated.reasons.clear();
return Literal{true, addConditionalConstraint(negated)};
}
} }
else else
return ~_lit; return ~_lit;