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

mark rational encoding problems

Browse Source
This commit is contained in:
chriseth 2022-05-12 10:26:57 +02:00
parent 074969b5d9
commit 7b0e02b1ff
1 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolutil/BooleanLP.cpp
View File

@ -307,7 +307,10 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
else if (_expr.name == ">=") else if (_expr.name == ">=")
addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings)); addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings));
else if (_expr.name == "<") else if (_expr.name == "<")
{
cerr << "ERROR cannot properly encode '<'" << endl;
addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings)); addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings));
}
else if (_expr.name == ">") else if (_expr.name == ">")
addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings)); addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings));
else else
@ -384,14 +387,11 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
{ {
cerr << "ERROR cannot properly encode '<'" << endl; cerr << "ERROR cannot properly encode '<'" << endl;
// TODO this is not the theory of reals! // TODO this is not the theory of reals!
return parseLiteral(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings)); return parseLiteral(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings));
} }
else if (_expr.name == ">") else if (_expr.name == ">")
{
cerr << "ERROR cannot properly encode '>'" << endl;
// TODO this is not the theory of reals!
return parseLiteral(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings)); return parseLiteral(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings));
}
return {}; return {};
} }
@ -405,6 +405,8 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
{ {
// X = b // X = b
cerr << "ERROR cannot properly encode '<'" << endl;
// X <= b - 1 // X <= b - 1
Constraint le = c; Constraint le = c;
le.equality = false; le.equality = false;
@ -429,7 +431,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
} }
else else
{ {
// TODO We can only do this if we know it is an integer! cerr << "ERROR cannot properly encode '<'" << endl;
// X > b // X > b
// -x < -b // -x < -b
// -x <= -b - 1 // -x <= -b - 1