From c34019f13668fdca4d34da98e0386c451dcf6b1c Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 21 Mar 2022 10:34:53 +0100 Subject: [PATCH] Fix and and change some conditions. --- libsolutil/BooleanLP.cpp | 2 ++ libyul/optimiser/ReasoningBasedSimplifier.cpp | 17 +++++++++-------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 295d7d3c9..277091147 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -172,6 +172,8 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0))); state().clauses.emplace_back(Clause{vector{l}}); } + else if (_expr.name == "implies") + addAssertion(!_expr.arguments.at(0) || _expr.arguments.at(1)); else if (_expr.name == "<=") { optional left = parseLinearSum(_expr.arguments.at(0)); diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index 189140ba9..cfe367c67 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -86,7 +86,7 @@ void ReasoningBasedSimplifier::operator()(If& _if) cout << "Checking if condition can be true" << endl; m_solver->push(); // TODO change this to >= 1 for simplicity? - m_solver->addAssertion(condition != constantValue(0)); + m_solver->addAssertion(condition >= 1); cout << " running check" << endl; CheckResult result2 = m_solver->check({}).first; m_solver->pop(); @@ -105,7 +105,7 @@ void ReasoningBasedSimplifier::operator()(If& _if) m_solver->push(); cout << "Setting condition true inside body" << endl; - m_solver->addAssertion(condition != constantValue(0)); + m_solver->addAssertion(condition >= constantValue(1)); ASTModifier::operator()(_if.body); @@ -264,12 +264,13 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin( case evmasm::Instruction::ISZERO: return booleanValue(arguments.at(0) == constantValue(0)); case evmasm::Instruction::AND: - return smtutil::Expression::ite( - arguments.at(0) + arguments.at(1) <= 2, - booleanValue(arguments.at(0) + arguments.at(1) >= 2), - // TODO we could probably restrict it a bit more - newRestrictedVariable() - ); + { + smtutil::Expression result = newRestrictedVariable(); + m_solver->addAssertion(result <= arguments.at(0)); + m_solver->addAssertion(result <= arguments.at(1)); + // TODO can we say more? + return result; + } case evmasm::Instruction::OR: return smtutil::Expression::ite( arguments.at(0) + arguments.at(1) <= 2,