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

Support all fractional constants.

Browse Source
This commit is contained in:
chriseth 2022-06-01 17:53:33 +02:00
parent cd3b7e333d
commit 68bfbdb2a6
2 changed files with 38 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
libsolutil/BooleanLP.cpp
View File

@ -411,8 +411,6 @@ void BooleanLPSolver::addLetBindings(Expression const& _let, LetBindings& _letBi
optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, LetBindings _letBindings) optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, LetBindings _letBindings)
{ {
// TODO constanst true/false?
if (_expr.name == "let") if (_expr.name == "let")
{ {
addLetBindings(_expr, _letBindings); addLetBindings(_expr, _letBindings);
@ -430,6 +428,11 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
else else
varIndex = std::get<size_t>(binding); varIndex = std::get<size_t>(binding);
} }
else if (_expr.name == "true" || _expr.name == "false")
{
// TODO handle this better
solAssert(false, "True/false literals not implemented");
}
else else
varIndex = state().variables.at(_expr.name); varIndex = state().variables.at(_expr.name);
solAssert(isBooleanVariable(varIndex)); solAssert(isBooleanVariable(varIndex));
@ -594,7 +597,7 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
// This will result in nullopt unless one of them is a constant. // This will result in nullopt unless one of them is a constant.
return parseLinearSum(_expr.arguments.at(0), _letBindings) * parseLinearSum(_expr.arguments.at(1), _letBindings); return parseLinearSum(_expr.arguments.at(0), _letBindings) * parseLinearSum(_expr.arguments.at(1), _letBindings);
} }
else if (_expr.name == "/") else if (_expr.name == "/" || _expr.name == "div")
{ {
solAssert(_expr.arguments.size() == 2); solAssert(_expr.arguments.size() == 2);
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings); optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
@ -614,19 +617,42 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
} }
else else
{ {
cerr << _expr.toString() << endl; // cerr << _expr.toString() << endl;
cerr << "Invalid operator " << _expr.name << endl; // cerr << "Invalid operator " << _expr.name << endl;
return std::nullopt; return std::nullopt;
} }
} }
namespace
{
bool isNumber(string const& _expr)
{
return !_expr.empty() && (isDigit(_expr.front()) || _expr.front() == '.');
}
rational parseRational(string const& _atom)
{
size_t decimal = _atom.find('.');
if (decimal == string::npos)
return rational(bigint(_atom));
unsigned shift = static_cast<unsigned>(_atom.size() - decimal - 1);
rational r(
bigint(string(_atom.substr(0, decimal)) + string(_atom.substr(decimal + 1))),
pow(bigint(10), shift)
);
// cerr << _atom << endl;
// cerr << r << endl;
return r;
}
}
bool BooleanLPSolver::isLiteral(smtutil::Expression const& _expr) const bool BooleanLPSolver::isLiteral(smtutil::Expression const& _expr) const
{ {
if (!_expr.arguments.empty()) if (!_expr.arguments.empty())
return false; return false;
solAssert(!_expr.name.empty(), ""); solAssert(!_expr.name.empty(), "");
return return
('0' <= _expr.name[0] && _expr.name[0] <= '9') || isNumber(_expr.name) ||
_expr.name == "true" || _expr.name == "true" ||
_expr.name == "false"; _expr.name == "false";
} }
@ -635,8 +661,8 @@ optional<LinearExpression> BooleanLPSolver::parseFactor(smtutil::Expression cons
{ {
solAssert(_expr.arguments.empty(), ""); solAssert(_expr.arguments.empty(), "");
solAssert(!_expr.name.empty(), ""); solAssert(!_expr.name.empty(), "");
if ('0' <= _expr.name[0] && _expr.name[0] <= '9') if (isNumber(_expr.name))
return LinearExpression::constant(rational(bigint(_expr.name))); return LinearExpression::constant(parseRational(_expr.name));
else if (_expr.name == "true") else if (_expr.name == "true")
// TODO do we want to do this? // TODO do we want to do this?
return LinearExpression::constant(1); return LinearExpression::constant(1);

15
tools/solsmt.cpp
View File

@ -129,21 +129,14 @@ string_view command(SMTLib2Expression const& _expr)
return get<string_view>(items.front().data); return get<string_view>(items.front().data);
} }
// TODO If we want to return rational here, we need smtutil::Expression to support rationals...
u256 parseRational(string_view _atom)
{
if (_atom.size() >= 3 && _atom.at(_atom.size() - 1) == '0' && _atom.at(_atom.size() - 2) == '.')
return parseRational(_atom.substr(0, _atom.size() - 2));
else
return u256(_atom);
}
smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<string, SortPointer> const& _variableSorts) smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<string, SortPointer> const& _variableSorts)
{ {
return std::visit(GenericVisitor{ return std::visit(GenericVisitor{
[&](string_view const& _atom) { [&](string_view const& _atom) {
if (isDigit(_atom.front()) || _atom.front() == '.') if (_atom == "true" || _atom == "false")
return Expression(parseRational(_atom).str(), {}, SortProvider::realSort); return Expression(_atom == "true");
else if (isDigit(_atom.front()) || _atom.front() == '.')
return Expression(string(_atom), {}, SortProvider::realSort);
else else
return Expression(string(_atom), {}, _variableSorts.at(string(_atom))); return Expression(string(_atom), {}, _variableSorts.at(string(_atom)));
}, },