From 24068116d98ec1186c336745efa6876422503160 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 21 Mar 2022 11:24:54 +0100 Subject: [PATCH] Simplify conditions. --- libyul/optimiser/ReasoningBasedSimplifier.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index 2bedd8733..636c75ba5 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -118,7 +118,7 @@ void ReasoningBasedSimplifier::operator()(ForLoop& _for) cout << "Checking if condition can be false" << endl; smtutil::Expression condition = encodeExpression(*_for.condition); m_solver->push(); - m_solver->addAssertion(condition == constantValue(0)); + m_solver->addAssertion(condition <= constantValue(0)); cout << " running check" << endl; CheckResult result = m_solver->check({}).first; m_solver->pop(); @@ -133,7 +133,7 @@ void ReasoningBasedSimplifier::operator()(ForLoop& _for) { cout << "Checking if condition can be true" << endl; m_solver->push(); - m_solver->addAssertion(condition != constantValue(0)); + m_solver->addAssertion(condition >= constantValue(1)); cout << " running check" << endl; CheckResult result2 = m_solver->check({}).first; m_solver->pop(); @@ -151,7 +151,7 @@ void ReasoningBasedSimplifier::operator()(ForLoop& _for) m_solver->push(); cout << "Setting condition true inside body" << endl; - m_solver->addAssertion(condition != constantValue(0)); + m_solver->addAssertion(condition >= constantValue(1)); ASTModifier::operator()(_for.body); ASTModifier::operator()(_for.post); @@ -325,7 +325,8 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin( smtutil::Expression ReasoningBasedSimplifier::newZeroOneVariable() { smtutil::Expression var = newVariable(); - m_solver->addAssertion(var == 0 || var == 1); + m_solver->addAssertion(var <= 1); + m_solver->addAssertion(var <= 0 || var >= 1); return var; }