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 and and change some conditions.

Browse Source
This commit is contained in:
chriseth 2022-03-21 10:34:53 +01:00
parent a3f999a13e
commit c34019f136
2 changed files with 11 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolutil/BooleanLP.cpp
View File

@ -172,6 +172,8 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0))); Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));
state().clauses.emplace_back(Clause{vector<Literal>{l}}); state().clauses.emplace_back(Clause{vector<Literal>{l}});
} }
else if (_expr.name == "implies")
addAssertion(!_expr.arguments.at(0) || _expr.arguments.at(1));
else if (_expr.name == "<=") else if (_expr.name == "<=")
{ {
optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0)); optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0));

17
libyul/optimiser/ReasoningBasedSimplifier.cpp
View File

@ -86,7 +86,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
cout << "Checking if condition can be true" << endl; cout << "Checking if condition can be true" << endl;
m_solver->push(); m_solver->push();
// TODO change this to >= 1 for simplicity? // TODO change this to >= 1 for simplicity?
m_solver->addAssertion(condition != constantValue(0)); m_solver->addAssertion(condition >= 1);
cout << " running check" << endl; cout << " running check" << endl;
CheckResult result2 = m_solver->check({}).first; CheckResult result2 = m_solver->check({}).first;
m_solver->pop(); m_solver->pop();
@ -105,7 +105,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
m_solver->push(); m_solver->push();
cout << "Setting condition true inside body" << endl; cout << "Setting condition true inside body" << endl;
m_solver->addAssertion(condition != constantValue(0)); m_solver->addAssertion(condition >= constantValue(1));
ASTModifier::operator()(_if.body); ASTModifier::operator()(_if.body);
@ -264,12 +264,13 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
case evmasm::Instruction::ISZERO: case evmasm::Instruction::ISZERO:
return booleanValue(arguments.at(0) == constantValue(0)); return booleanValue(arguments.at(0) == constantValue(0));
case evmasm::Instruction::AND: case evmasm::Instruction::AND:
return smtutil::Expression::ite( {
arguments.at(0) + arguments.at(1) <= 2, smtutil::Expression result = newRestrictedVariable();
booleanValue(arguments.at(0) + arguments.at(1) >= 2), m_solver->addAssertion(result <= arguments.at(0));
// TODO we could probably restrict it a bit more m_solver->addAssertion(result <= arguments.at(1));
newRestrictedVariable() // TODO can we say more?
); return result;
}
case evmasm::Instruction::OR: case evmasm::Instruction::OR:
return smtutil::Expression::ite( return smtutil::Expression::ite(
arguments.at(0) + arguments.at(1) <= 2, arguments.at(0) + arguments.at(1) <= 2,