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

Better assertions for boolean lp.

Browse Source
This commit is contained in:
chriseth 2022-05-09 17:22:38 +02:00
parent dc6eecd4ba
commit 3e36c97367
2 changed files with 23 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
libsolutil/BooleanLP.cpp
View File

@ -441,9 +441,9 @@ Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _exp
optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr) optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr)
{ {
if (_expr.arguments.empty() || _expr.name == "*") if (_expr.arguments.empty())
return parseProduct(_expr); return parseFactor(_expr);
else if (_expr.name == "+" || _expr.name == "-") else if (_expr.name == "+" || (_expr.name == "-" && _expr.arguments.size() == 2))
{ {
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));
@ -451,6 +451,26 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
return std::nullopt; return std::nullopt;
return _expr.name == "+" ? *left + *right : *left - *right; return _expr.name == "+" ? *left + *right : *left - *right;
} }
else if (_expr.name == "-" && _expr.arguments.size() == 1)
{
optional<LinearExpression> arg = parseLinearSum(_expr.arguments.at(0));
if (arg)
return LinearExpression::constant(0) - *arg;
else
return std::nullopt;
}
else if (_expr.name == "*")
// This will result in nullopt unless one of them is a constant.
return parseLinearSum(_expr.arguments.at(0)) * parseLinearSum(_expr.arguments.at(1));
else if (_expr.name == "/")
{
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0));
optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1));
if (!left || !right || !right->isConstant())
return std::nullopt;
*left /= right->get(0);
return left;
}
else if (_expr.name == "ite") else if (_expr.name == "ite")
{ {
Expression result = declareInternalVariable(false); Expression result = declareInternalVariable(false);

2
libsolutil/BooleanLP.h
View File

@ -78,8 +78,6 @@ public:
std::pair<smtutil::CheckResult, std::vector<std::string>> std::pair<smtutil::CheckResult, std::vector<std::string>>
check(std::vector<smtutil::Expression> const& _expressionsToEvaluate) override; check(std::vector<smtutil::Expression> const& _expressionsToEvaluate) override;
std::pair<smtutil::CheckResult, std::map<std::string, boost::rational<bigint>>> check();
std::string toString() const; std::string toString() const;
private: private: