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 toString.

Browse Source
This commit is contained in:
chriseth 2022-05-30 11:08:16 +02:00
parent 62051ade2b
commit e655f53813
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolutil/BooleanLP.cpp
View File

@ -172,6 +172,9 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
Clause conflictClause; Clause conflictClause;
for (size_t constraintIndex: reasonSet) for (size_t constraintIndex: reasonSet)
conflictClause.emplace_back(Literal{false, constraintIndex}); conflictClause.emplace_back(Literal{false, constraintIndex});
#ifdef DEBUG
cerr << "||||| conflict claus: " << toString(conflictClause) << endl;
#endif
return conflictClause; return conflictClause;
} }
else else
@ -755,14 +758,17 @@ string BooleanLPSolver::toString(Clause const& _clause) const
{ {
vector<string> literals; vector<string> literals;
for (Literal const& l: _clause) for (Literal const& l: _clause)
{
string lit = l.positive ? "" : "!";
if (isBooleanVariable(l.variable)) if (isBooleanVariable(l.variable))
literals.emplace_back((l.positive ? "" : "!") + variableName(l.variable)); lit += variableName(l.variable);
else else
{ {
solAssert(isConditionalConstraint(l.variable)); solAssert(isConditionalConstraint(l.variable));
solAssert(l.positive); lit += toString(conditionalConstraint(l.variable));
literals.emplace_back(toString(conditionalConstraint(l.variable)));
} }
literals.emplace_back(move(lit));
}
return joinHumanReadable(literals, " \\/ ") + "\n"; return joinHumanReadable(literals, " \\/ ") + "\n";
} }