Remove ReasoningBasedSimplifier from libyul

Due to a design decision to move away from a bundled SMT solver,
ReasoningBasedSimplifier in its current form cannot be use any longer.
This is a necessary step to allow a unified way to call solvers using
only SMTLIB interface.

Since this optimization pass has always been marked as highly
experimental and never turned on by default, it should be OK to remove
it.

Changelog.md

@@ -12,6 +12,7 @@ Compiler Features:
  * SMTChecker: Add ``--model-checker-print-query`` CLI option and ``settings.modelChecker.printQuery`` JSON option to output the SMTChecker queries in the SMTLIB2 format. This requires using `smtlib2` solver only.
  * Standard JSON Interface: Add ``ast`` file-level output for Yul input.
  * Standard JSON Interface: Add ``irAst`` and ``irOptimizedAst`` contract-level outputs for Solidity input, providing AST in compact JSON format for IR and optimized IR.
+ * Yul Optimizer: Remove experimental `ReasoningBasedSimplifier` optimization step.
  * Yul Optimizer: Stack-to-memory mover is now enabled by default whenever possible for via IR code generation and pure Yul compilation.
 
 

docs/internals/optimizer.rst

@@ -316,7 +316,6 @@ Abbreviation Full name
 ``L``        :ref:`load-resolver`
 ``M``        :ref:`loop-invariant-code-motion`
 ``r``        :ref:`redundant-assign-eliminator`
-``R``        :ref:`reasoning-based-simplifier` - highly experimental
 ``m``        :ref:`rematerialiser`
 ``V``        :ref:`SSA-reverser`
 ``a``        :ref:`SSA-transform`
@@ -330,10 +329,6 @@ Abbreviation Full name
 Some steps depend on properties ensured by ``BlockFlattener``, ``FunctionGrouper``, ``ForLoopInitRewriter``.
 For this reason the Yul optimizer always applies them before applying any steps supplied by the user.
 
-The ReasoningBasedSimplifier is an optimizer step that is currently not enabled
-in the default set of steps. It uses an SMT solver to simplify arithmetic expressions
-and boolean conditions. It has not received thorough testing or validation yet and can produce
-non-reproducible results, so please use with care!
 
 Selecting Optimizations
 -----------------------
@@ -863,22 +858,6 @@ Works best if the code is in SSA form.
 
 Prerequisite: Disambiguator, ForLoopInitRewriter.
 
-.. _reasoning-based-simplifier:
-
-ReasoningBasedSimplifier
-^^^^^^^^^^^^^^^^^^^^^^^^
-
-This optimizer uses SMT solvers to check whether ``if`` conditions are constant.
-
-- If ``constraints AND condition`` is UNSAT, the condition is never true and the whole body can be removed.
-- If ``constraints AND NOT condition`` is UNSAT, the condition is always true and can be replaced by ``1``.
-
-The simplifications above can only be applied if the condition is movable.
-
-It is only effective on the EVM dialect, but safe to use on other dialects.
-
-Prerequisite: Disambiguator, SSATransform.
-
 Statement-Scale Simplifications
 -------------------------------
 

libyul/CMakeLists.txt

@@ -143,8 +143,6 @@ add_library(yul
 	optimiser/OptimiserStep.h
 	optimiser/OptimizerUtilities.cpp
 	optimiser/OptimizerUtilities.h
-	optimiser/ReasoningBasedSimplifier.cpp
-	optimiser/ReasoningBasedSimplifier.h
 	optimiser/UnusedAssignEliminator.cpp
 	optimiser/UnusedAssignEliminator.h
 	optimiser/UnusedStoreBase.cpp
@@ -153,8 +151,6 @@ add_library(yul
 	optimiser/UnusedStoreEliminator.h
 	optimiser/Rematerialiser.cpp
 	optimiser/Rematerialiser.h
-	optimiser/SMTSolver.cpp
-	optimiser/SMTSolver.h
 	optimiser/SSAReverser.cpp
 	optimiser/SSAReverser.h
 	optimiser/SSATransform.cpp

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -1,228 +0,0 @@
-/*
-	This file is part of solidity.
-
-	solidity is free software: you can redistribute it and/or modify
-	it under the terms of the GNU General Public License as published by
-	the Free Software Foundation, either version 3 of the License, or
-	(at your option) any later version.
-
-	solidity is distributed in the hope that it will be useful,
-	but WITHOUT ANY WARRANTY; without even the implied warranty of
-	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-	GNU General Public License for more details.
-
-	You should have received a copy of the GNU General Public License
-	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
-*/
-
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
-#include <libyul/optimiser/SMTSolver.h>
-
-#include <libyul/optimiser/SSAValueTracker.h>
-#include <libyul/optimiser/Semantics.h>
-#include <libyul/AST.h>
-#include <libyul/Dialect.h>
-
-#include <libsmtutil/SMTPortfolio.h>
-#include <libsmtutil/Helpers.h>
-
-#include <libsolutil/CommonData.h>
-
-#include <libevmasm/Instruction.h>
-
-#include <utility>
-#include <memory>
-
-using namespace std;
-using namespace solidity;
-using namespace solidity::util;
-using namespace solidity::yul;
-using namespace solidity::smtutil;
-
-void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
-{
-	set<YulString> ssaVars = SSAValueTracker::ssaVariables(_ast);
-	ReasoningBasedSimplifier{_context.dialect, ssaVars}(_ast);
-}
-
-std::optional<string> ReasoningBasedSimplifier::invalidInCurrentEnvironment()
-{
-	// SMTLib2 interface is always available, but we would like to have synchronous answers.
-	if (smtutil::SMTPortfolio{}.solvers() <= 1)
-		return string{"No SMT solvers available."};
-	else
-		return nullopt;
-}
-
-void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl)
-{
-	SMTSolver::encodeVariableDeclaration(_varDecl);
-}
-
-void ReasoningBasedSimplifier::operator()(If& _if)
-{
-	if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
-		return;
-
-	smtutil::Expression condition = encodeExpression(*_if.condition);
-	m_solver->push();
-	m_solver->addAssertion(condition == constantValue(0));
-	CheckResult result = m_solver->check({}).first;
-	m_solver->pop();
-	if (result == CheckResult::UNSATISFIABLE)
-	{
-		Literal trueCondition = m_dialect.trueLiteral();
-		trueCondition.debugData = debugDataOf(*_if.condition);
-		_if.condition = make_unique<yul::Expression>(std::move(trueCondition));
-	}
-	else
-	{
-		m_solver->push();
-		m_solver->addAssertion(condition != constantValue(0));
-		CheckResult result2 = m_solver->check({}).first;
-		m_solver->pop();
-		if (result2 == CheckResult::UNSATISFIABLE)
-		{
-			Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
-			falseCondition.debugData = debugDataOf(*_if.condition);
-			_if.condition = make_unique<yul::Expression>(std::move(falseCondition));
-			_if.body = yul::Block{};
-			// Nothing left to be done.
-			return;
-		}
-	}
-
-	m_solver->push();
-	m_solver->addAssertion(condition != constantValue(0));
-
-	ASTModifier::operator()(_if.body);
-
-	m_solver->pop();
-}
-
-ReasoningBasedSimplifier::ReasoningBasedSimplifier(
-	Dialect const& _dialect,
-	set<YulString> const& _ssaVariables
-):
-	SMTSolver(_ssaVariables, _dialect),
-	m_dialect(_dialect)
-{
-}
-
-
-smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
-	evmasm::Instruction _instruction,
-	vector<yul::Expression> const& _arguments
-)
-{
-	vector<smtutil::Expression> arguments = applyMap(
-		_arguments,
-		[this](yul::Expression const& _expr) { return encodeExpression(_expr); }
-	);
-	switch (_instruction)
-	{
-	case evmasm::Instruction::ADD:
-		return wrap(arguments.at(0) + arguments.at(1));
-	case evmasm::Instruction::MUL:
-		return wrap(arguments.at(0) * arguments.at(1));
-	case evmasm::Instruction::SUB:
-		return wrap(arguments.at(0) - arguments.at(1));
-	case evmasm::Instruction::DIV:
-		return smtutil::Expression::ite(
-			arguments.at(1) == constantValue(0),
-			constantValue(0),
-			arguments.at(0) / arguments.at(1)
-		);
-	case evmasm::Instruction::SDIV:
-		return smtutil::Expression::ite(
-			arguments.at(1) == constantValue(0),
-			constantValue(0),
-			// No `wrap()` needed here, because -2**255 / -1 results
-			// in 2**255 which is "converted" to its two's complement
-			// representation 2**255 in `signedToTwosComplement`
-			signedToTwosComplement(smtutil::signedDivisionEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
-			))
-		);
-	case evmasm::Instruction::MOD:
-		return smtutil::Expression::ite(
-			arguments.at(1) == constantValue(0),
-			constantValue(0),
-			arguments.at(0) % arguments.at(1)
-		);
-	case evmasm::Instruction::SMOD:
-		return smtutil::Expression::ite(
-			arguments.at(1) == constantValue(0),
-			constantValue(0),
-			signedToTwosComplement(signedModuloEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
-			))
-		);
-	case evmasm::Instruction::LT:
-		return booleanValue(arguments.at(0) < arguments.at(1));
-	case evmasm::Instruction::SLT:
-		return booleanValue(twosComplementToSigned(arguments.at(0)) < twosComplementToSigned(arguments.at(1)));
-	case evmasm::Instruction::GT:
-		return booleanValue(arguments.at(0) > arguments.at(1));
-	case evmasm::Instruction::SGT:
-		return booleanValue(twosComplementToSigned(arguments.at(0)) > twosComplementToSigned(arguments.at(1)));
-	case evmasm::Instruction::EQ:
-		return booleanValue(arguments.at(0) == arguments.at(1));
-	case evmasm::Instruction::ISZERO:
-		return booleanValue(arguments.at(0) == constantValue(0));
-	case evmasm::Instruction::AND:
-		return smtutil::Expression::ite(
-			(arguments.at(0) == 0 || arguments.at(0) == 1) &&
-			(arguments.at(1) == 0 || arguments.at(1) == 1),
-			booleanValue(arguments.at(0) == 1 && arguments.at(1) == 1),
-			bv2int(int2bv(arguments.at(0)) & int2bv(arguments.at(1)))
-		);
-	case evmasm::Instruction::OR:
-		return smtutil::Expression::ite(
-			(arguments.at(0) == 0 || arguments.at(0) == 1) &&
-			(arguments.at(1) == 0 || arguments.at(1) == 1),
-			booleanValue(arguments.at(0) == 1 || arguments.at(1) == 1),
-			bv2int(int2bv(arguments.at(0)) | int2bv(arguments.at(1)))
-		);
-	case evmasm::Instruction::XOR:
-		return bv2int(int2bv(arguments.at(0)) ^ int2bv(arguments.at(1)));
-	case evmasm::Instruction::NOT:
-		return smtutil::Expression(u256(-1)) - arguments.at(0);
-	case evmasm::Instruction::SHL:
-		return smtutil::Expression::ite(
-			arguments.at(0) > 255,
-			constantValue(0),
-			bv2int(int2bv(arguments.at(1)) << int2bv(arguments.at(0)))
-		);
-	case evmasm::Instruction::SHR:
-		return smtutil::Expression::ite(
-			arguments.at(0) > 255,
-			constantValue(0),
-			bv2int(int2bv(arguments.at(1)) >> int2bv(arguments.at(0)))
-		);
-	case evmasm::Instruction::SAR:
-		return smtutil::Expression::ite(
-			arguments.at(0) > 255,
-			constantValue(0),
-			bv2int(smtutil::Expression::ashr(int2bv(arguments.at(1)), int2bv(arguments.at(0))))
-		);
-	case evmasm::Instruction::ADDMOD:
-		return smtutil::Expression::ite(
-			arguments.at(2) == constantValue(0),
-			constantValue(0),
-			(arguments.at(0) + arguments.at(1)) % arguments.at(2)
-		);
-	case evmasm::Instruction::MULMOD:
-		return smtutil::Expression::ite(
-			arguments.at(2) == constantValue(0),
-			constantValue(0),
-			(arguments.at(0) * arguments.at(1)) % arguments.at(2)
-		);
-	// TODO SIGNEXTEND
-	default:
-		break;
-	}
-	return newRestrictedVariable();
-}

libyul/optimiser/ReasoningBasedSimplifier.h

@@ -1,75 +0,0 @@
-/*
-	This file is part of solidity.
-
-	solidity is free software: you can redistribute it and/or modify
-	it under the terms of the GNU General Public License as published by
-	the Free Software Foundation, either version 3 of the License, or
-	(at your option) any later version.
-
-	solidity is distributed in the hope that it will be useful,
-	but WITHOUT ANY WARRANTY; without even the implied warranty of
-	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-	GNU General Public License for more details.
-
-	You should have received a copy of the GNU General Public License
-	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
-*/
-#pragma once
-
-#include <libyul/optimiser/SMTSolver.h>
-#include <libyul/optimiser/ASTWalker.h>
-#include <libyul/optimiser/OptimiserStep.h>
-#include <libyul/Dialect.h>
-
-// because of instruction
-#include <libyul/backends/evm/EVMDialect.h>
-
-#include <map>
-
-namespace solidity::smtutil
-{
-class SolverInterface;
-class Expression;
-struct Sort;
-}
-
-namespace solidity::yul
-{
-
-/**
- * Reasoning-based simplifier.
- * This optimizer uses SMT solvers to check whether `if` conditions are constant.
- * - If `constraints AND condition` is UNSAT, the condition is never true and the whole body can be removed.
- * - If `constraints AND NOT condition` is UNSAT, the condition is always true and can be replaced by `1`.
- * The simplifications above can only be applied if the condition is movable.
- *
- * It is only effective on the EVM dialect, but safe to use on other dialects.
- *
- * Prerequisite: Disambiguator, SSATransform.
- */
-class ReasoningBasedSimplifier: public ASTModifier, SMTSolver
-{
-public:
-	static constexpr char const* name{"ReasoningBasedSimplifier"};
-	static void run(OptimiserStepContext& _context, Block& _ast);
-	static std::optional<std::string> invalidInCurrentEnvironment();
-
-	using ASTModifier::operator();
-	void operator()(VariableDeclaration& _varDecl) override;
-	void operator()(If& _if) override;
-
-private:
-	explicit ReasoningBasedSimplifier(
-		Dialect const& _dialect,
-		std::set<YulString> const& _ssaVariables
-	);
-
-	smtutil::Expression encodeEVMBuiltin(
-		evmasm::Instruction _instruction,
-		std::vector<Expression> const& _arguments
-	) override;
-
-	Dialect const& m_dialect;
-};
-
-}

libyul/optimiser/SMTSolver.cpp

@@ -1,160 +0,0 @@
-/*
-	This file is part of solidity.
-
-	solidity is free software: you can redistribute it and/or modify
-	it under the terms of the GNU General Public License as published by
-	the Free Software Foundation, either version 3 of the License, or
-	(at your option) any later version.
-
-	solidity is distributed in the hope that it will be useful,
-	but WITHOUT ANY WARRANTY; without even the implied warranty of
-	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-	GNU General Public License for more details.
-
-	You should have received a copy of the GNU General Public License
-	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
-*/
-
-#include <libyul/optimiser/SMTSolver.h>
-#include <libyul/optimiser/OptimizerUtilities.h>
-
-#include <libyul/AST.h>
-#include <libyul/Utilities.h>
-
-#include <libsolutil/Visitor.h>
-#include <libsolutil/CommonData.h>
-
-#include <libsmtutil/SMTPortfolio.h>
-#include <libsmtutil/Helpers.h>
-
-using namespace solidity::yul;
-using namespace solidity::util;
-using namespace solidity::smtutil;
-using namespace solidity;
-using namespace std;
-
-SMTSolver::SMTSolver(set<YulString> const& _ssaVariables, Dialect const& _dialect):
-	m_ssaVariables(_ssaVariables),
-	m_solver(make_unique<smtutil::SMTPortfolio>()),
-	m_dialect(_dialect)
-{ }
-
-smtutil::Expression SMTSolver::encodeExpression(Expression const& _expression)
-{
-	return std::visit(GenericVisitor{
-		[&](FunctionCall const& _functionCall)
-		{
-			if (auto instruction = toEVMInstruction(m_dialect, _functionCall.functionName.name))
-				return encodeEVMBuiltin(*instruction, _functionCall.arguments);
-
-			return newRestrictedVariable();
-		},
-		[&](Identifier const& _identifier)
-		{
-			if (
-				m_ssaVariables.count(_identifier.name) &&
-				m_variables.count(_identifier.name)
-			)
-				return m_variables.at(_identifier.name);
-			else
-				return newRestrictedVariable();
-		},
-		[&](Literal const& _literal)
-		{
-			return literalValue(_literal);
-		}
-	}, _expression);
-}
-
-smtutil::Expression SMTSolver::int2bv(smtutil::Expression _arg)
-{
-	return smtutil::Expression::int2bv(std::move(_arg), 256);
-}
-
-smtutil::Expression SMTSolver::bv2int(smtutil::Expression _arg)
-{
-	return smtutil::Expression::bv2int(std::move(_arg));
-}
-
-smtutil::Expression SMTSolver::newVariable()
-{
-	return m_solver->newVariable(uniqueName(), defaultSort());
-}
-
-smtutil::Expression SMTSolver::newRestrictedVariable(bigint _maxValue)
-{
-	smtutil::Expression var = newVariable();
-	m_solver->addAssertion(0 <= var && var <= smtutil::Expression(_maxValue));
-	return var;
-}
-
-string SMTSolver::uniqueName()
-{
-	return "expr_" + to_string(m_varCounter++);
-}
-
-shared_ptr<Sort> SMTSolver::defaultSort() const
-{
-	return SortProvider::intSort();
-}
-
-smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
-}
-
-smtutil::Expression SMTSolver::constantValue(bigint _value)
-{
-	return _value;
-}
-
-smtutil::Expression SMTSolver::literalValue(Literal const& _literal)
-{
-	return smtutil::Expression(valueOfLiteral(_literal));
-}
-
-smtutil::Expression SMTSolver::twosComplementToSigned(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(
-		_value < smtutil::Expression(bigint(1) << 255),
-		_value,
-		_value - smtutil::Expression(bigint(1) << 256)
-	);
-}
-
-smtutil::Expression SMTSolver::signedToTwosComplement(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(
-		_value >= 0,
-		_value,
-		_value + smtutil::Expression(bigint(1) << 256)
-	);
-}
-
-smtutil::Expression SMTSolver::wrap(smtutil::Expression _value)
-{
-	smtutil::Expression rest = newRestrictedVariable();
-	smtutil::Expression multiplier = newVariable();
-	m_solver->addAssertion(_value == multiplier * smtutil::Expression(bigint(1) << 256) + rest);
-	return rest;
-}
-
-void SMTSolver::encodeVariableDeclaration(VariableDeclaration const& _varDecl)
-{
-	if (
-		_varDecl.variables.size() == 1 &&
-		_varDecl.value &&
-		m_ssaVariables.count(_varDecl.variables.front().name)
-	)
-	{
-		YulString const& variableName = _varDecl.variables.front().name;
-		bool const inserted = m_variables.insert({
-			variableName,
-			m_solver->newVariable("yul_" + variableName.str(), defaultSort())
-		}).second;
-		yulAssert(inserted, "");
-		m_solver->addAssertion(
-			m_variables.at(variableName) == encodeExpression(*_varDecl.value)
-		);
-	}
-}

libyul/optimiser/SMTSolver.h

@@ -1,92 +0,0 @@
-/*
-	This file is part of solidity.
-
-	solidity is free software: you can redistribute it and/or modify
-	it under the terms of the GNU General Public License as published by
-	the Free Software Foundation, either version 3 of the License, or
-	(at your option) any later version.
-
-	solidity is distributed in the hope that it will be useful,
-	but WITHOUT ANY WARRANTY; without even the implied warranty of
-	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-	GNU General Public License for more details.
-
-	You should have received a copy of the GNU General Public License
-	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
-*/
-#pragma once
-
-#include <libyul/AST.h>
-#include <libyul/Dialect.h>
-#include <libyul/Exceptions.h>
-
-// because of instruction
-#include <libyul/backends/evm/EVMDialect.h>
-
-#include <libsmtutil/SolverInterface.h>
-
-#include <memory>
-
-namespace solidity::smtutil
-{
-
-class SolverInterface;
-class Expression;
-struct Sort;
-
-}
-
-namespace solidity::yul
-{
-
-/**
- * Base class for SMT based optimization steps.
- *
- * Works best when used with AST in SSA form.
- */
-class SMTSolver
-{
-protected:
-	SMTSolver(
-		std::set<YulString> const& _ssaVariables,
-		Dialect const& _dialect
-	);
-
-	/// Helper function that encodes VariableDeclaration
-	void encodeVariableDeclaration(VariableDeclaration const& _varDecl);
-
-	/// The encoding for a builtin. The type of encoding determines what we are
-	/// solving for.
-	virtual smtutil::Expression encodeEVMBuiltin(
-		evmasm::Instruction _instruction,
-		std::vector<Expression> const& _arguments
-	) = 0;
-
-	smtutil::Expression encodeExpression(Expression const& _expression);
-
-	static smtutil::Expression int2bv(smtutil::Expression _arg);
-	static smtutil::Expression bv2int(smtutil::Expression _arg);
-
-	smtutil::Expression newVariable();
-	virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256) - 1);
-	std::string uniqueName();
-
-	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
-	static smtutil::Expression booleanValue(smtutil::Expression _value);
-	static smtutil::Expression constantValue(bigint _value);
-	static smtutil::Expression literalValue(Literal const& _literal);
-	static smtutil::Expression twosComplementToSigned(smtutil::Expression _value);
-	static smtutil::Expression signedToTwosComplement(smtutil::Expression _value);
-	smtutil::Expression wrap(smtutil::Expression _value);
-
-	std::set<YulString> const& m_ssaVariables;
-	std::unique_ptr<smtutil::SolverInterface> m_solver;
-	std::map<YulString, smtutil::Expression> m_variables;
-
-	Dialect const& m_dialect;
-
-private:
-	size_t m_varCounter = 0;
-};
-
-}

libyul/optimiser/Suite.cpp

@@ -43,7 +43,6 @@
 #include <libyul/optimiser/ForLoopInitRewriter.h>
 #include <libyul/optimiser/ForLoopConditionIntoBody.h>
 #include <libyul/optimiser/FunctionSpecializer.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/UnusedFunctionParameterPruner.h>
 #include <libyul/optimiser/UnusedPruner.h>
@@ -272,7 +271,6 @@ map<string, unique_ptr<OptimiserStep>> const& OptimiserSuite::allSteps()
 			LoopInvariantCodeMotion,
 			UnusedAssignEliminator,
 			UnusedStoreEliminator,
-			ReasoningBasedSimplifier,
 			Rematerialiser,
 			SSAReverser,
 			SSATransform,
@@ -312,7 +310,6 @@ map<string, char> const& OptimiserSuite::stepNameToAbbreviationMap()
 		{LiteralRematerialiser::name,         'T'},
 		{LoadResolver::name,                  'L'},
 		{LoopInvariantCodeMotion::name,       'M'},
-		{ReasoningBasedSimplifier::name,      'R'},
 		{UnusedAssignEliminator::name,        'r'},
 		{UnusedStoreEliminator::name,         'S'},
 		{Rematerialiser::name,                'm'},

test/libyul/YulOptimizerTest.cpp

@@ -24,7 +24,6 @@
 #include <test/Common.h>
 
 #include <libyul/Object.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/AsmPrinter.h>
 
 #include <liblangutil/CharStreamProvider.h>
@@ -53,12 +52,6 @@ YulOptimizerTest::YulOptimizerTest(string const& _filename):
 		BOOST_THROW_EXCEPTION(runtime_error("Filename path has to contain a directory: \"" + _filename + "\"."));
 	m_optimizerStep = std::prev(std::prev(path.end()))->string();
 
-	if (m_optimizerStep == "reasoningBasedSimplifier" && (
-		solidity::test::CommonOptions::get().disableSMT ||
-		ReasoningBasedSimplifier::invalidInCurrentEnvironment()
-	))
-		m_shouldRun = false;
-
 	m_source = m_reader.source();
 
 	auto dialectName = m_reader.stringSetting("dialect", "evm");

test/libyul/YulOptimizerTestCommon.cpp

@@ -49,7 +49,6 @@
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionJoiner.h>
 #include <libyul/optimiser/OptimiserStep.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/SSAReverser.h>
 #include <libyul/optimiser/SSATransform.h>
 #include <libyul/optimiser/Semantics.h>
@@ -289,10 +288,6 @@ YulOptimizerTestCommon::YulOptimizerTestCommon(
 			LiteralRematerialiser::run(*m_context, *m_ast);
 			StructuralSimplifier::run(*m_context, *m_ast);
 		}},
-		{"reasoningBasedSimplifier", [&]() {
-			disambiguate();
-			ReasoningBasedSimplifier::run(*m_context, *m_object->code);
-		}},
 		{"equivalentFunctionCombiner", [&]() {
 			disambiguate();
 			ForLoopInitRewriter::run(*m_context, *m_ast);
@@ -424,8 +419,7 @@ string YulOptimizerTestCommon::randomOptimiserStep(unsigned _seed)
 			// it can sometimes drain memory.
 			if (
 				optimiserStep == "mainFunction"	||
-				optimiserStep == "wordSizeTransform" ||
+				optimiserStep == "wordSizeTransform"
-				optimiserStep == "reasoningBasedSimplifier"
 			)
 				// "Fullsuite" is fuzzed roughly four times more frequently than
 				// other steps because of the filtering in place above.

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul

@@ -1,13 +0,0 @@
-{
-    let x := 7
-    let y := 8
-    if eq(add(x, y), 15) { }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let x := 7
-//     let y := 8
-//     if 1 { }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul

@@ -1,19 +0,0 @@
-{
-	function f() -> z
-	{
-		z := 15
-	}
-	let x := 7
-	let y := 8
-	if eq(add(x, y), f()) { }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     function f() -> z
-//     { z := 15 }
-//     let x := 7
-//     let y := 8
-//     if eq(add(x, y), f()) { }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul

@@ -1,23 +0,0 @@
-{
-	function f() -> z
-	{
-		sstore(1, 15)
-		z := 15
-	}
-	let x := 7
-	let y := 8
-	if eq(add(x, y), f()) { }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     function f() -> z
-//     {
-//         sstore(1, 15)
-//         z := 15
-//     }
-//     let x := 7
-//     let y := 8
-//     if eq(add(x, y), f()) { }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul

@@ -1,32 +0,0 @@
-{
-    let vloc_x := calldataload(0)
-    let vloc_y := calldataload(1)
-    if lt(vloc_x, shl(100, 1)) {
-        if lt(vloc_y, shl(100, 1)) {
-            if iszero(and(iszero(iszero(vloc_x)), gt(vloc_y, div(not(0), vloc_x)))) {
-                let vloc := mul(vloc_x, vloc_y)
-                sstore(0, vloc)
-            }
-        }
-    }
-}
-// ====
-// EVMVersion: >=constantinople
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let vloc_x := calldataload(0)
-//     let vloc_y := calldataload(1)
-//     if lt(vloc_x, shl(100, 1))
-//     {
-//         if lt(vloc_y, shl(100, 1))
-//         {
-//             if 1
-//             {
-//                 let vloc := mul(vloc_x, vloc_y)
-//                 sstore(0, vloc)
-//             }
-//         }
-//     }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul

@@ -1,31 +0,0 @@
-{
-    let x := calldataload(0)
-    let y := calldataload(32)
-    let z := calldataload(64)
-    let result := mulmod(x, y, z)
-
-    // should be zero
-    if gt(result, z) { sstore(0, 1) }
-
-    // mulmod is equal to mod of product for small numbers
-    if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) {
-        if eq(result, mod(mul(x, y), z)) { sstore(0, 9) }
-    }
-
-    // but not in general
-    if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) {
-        if eq(result, mod(mul(x, y), z)) { sstore(0, 5) }
-    }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let x := calldataload(0)
-//     let y := calldataload(32)
-//     let z := calldataload(64)
-//     let result := mulmod(x, y, z)
-//     if 0 { }
-//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } }
-//     if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { if 0 { } }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul

@@ -1,16 +0,0 @@
-{
-    let x := sub(0, 7)
-    let y := 2
-    // (-7)/2 == -3 on the evm
-    if iszero(add(sdiv(x, y), 3)) { }
-    if iszero(add(sdiv(x, y), 4)) { }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let x := sub(0, 7)
-//     let y := 2
-//     if 1 { }
-//     if 0 { }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul

@@ -1,26 +0,0 @@
-{
-    let x := calldataload(2)
-    let t := lt(x, 20)
-    if t {
-        if lt(x, 21) { }
-        if lt(x, 20) { }
-        if lt(x, 19) { }
-        if gt(x, 20) { }
-        if iszero(gt(x, 20)) { }
-    }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let x := calldataload(2)
-//     let t := lt(x, 20)
-//     if t
-//     {
-//         if 1 { }
-//         if 1 { }
-//         if lt(x, 19) { }
-//         if 0 { }
-//         if 1 { }
-//     }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul

@@ -1,31 +0,0 @@
-{
-    let y := calldataload(0)
-    let t := calldataload(32)
-
-    if sgt(sub(y, 1), y) {
-        // y - 1 > y, i.e. y is the most negative value
-        if eq(sdiv(y, sub(0, 1)), y) {
-            // should be true: y / -1 == y
-            sstore(0, 7)
-        }
-        if iszero(eq(y, t)) {
-            // t is not the most negative value
-            if eq(sdiv(t, sub(0, 1)), sub(0, t)) {
-                // should be true: t / -1 = 0 - t
-                sstore(1, 7)
-            }
-        }
-    }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let y := calldataload(0)
-//     let t := calldataload(32)
-//     if sgt(sub(y, 1), y)
-//     {
-//         if 1 { sstore(0, 7) }
-//         if iszero(eq(y, t)) { if 1 { sstore(1, 7) } }
-//     }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul

@@ -1,53 +0,0 @@
-{
-    // 7 % 5 == 2
-    // 7 % -5 == 2
-    // -7 % 5 == -2
-    // -7 % -5 == -2
-    // -5 % -5 == 0
-    let x := calldataload(0)
-    let y := calldataload(32)
-    let result := smod(x, y)
-    if eq(x, 7) {
-        if eq(y, 5) {
-            if eq(result, 2) { sstore(0, 7)}
-        }
-        if eq(y, sub(0, 5)) {
-            if eq(result, 2) { sstore(0, 7)}
-        }
-    }
-    if eq(x, sub(0, 7)) {
-        if eq(y, 5) {
-            if eq(result, sub(0, 2)) { sstore(0, 7)}
-        }
-        if eq(y, sub(0, 5)) {
-            if eq(result, sub(0, 2)) { sstore(0, 7)}
-        }
-    }
-    if eq(x, sub(0, 5)) {
-        if eq(y, sub(0, 5)) {
-            if eq(result, 0) { sstore(0, 7)}
-        }
-    }
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let x := calldataload(0)
-//     let y := calldataload(32)
-//     let result := smod(x, y)
-//     if eq(x, 7)
-//     {
-//         if eq(y, 5) { if 1 { sstore(0, 7) } }
-//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
-//     }
-//     if eq(x, sub(0, 7))
-//     {
-//         if eq(y, 5) { if 1 { sstore(0, 7) } }
-//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
-//     }
-//     if eq(x, sub(0, 5))
-//     {
-//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
-//     }
-// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul

@@ -1,5 +0,0 @@
-{ }
-// ----
-// step: reasoningBasedSimplifier
-//
-// { }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul

@@ -1,15 +0,0 @@
-{
-    let x := 7
-    let y := 8
-    if gt(sub(x, y), 20) { }
-    if eq(sub(x, y), 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) {}
-}
-// ----
-// step: reasoningBasedSimplifier
-//
-// {
-//     let x := 7
-//     let y := 8
-//     if 1 { }
-//     if 1 { }
-// }

test/tools/yulopti.cpp

@@ -37,7 +37,6 @@
 #include <libyul/optimiser/StackCompressor.h>
 #include <libyul/optimiser/VarNameCleaner.h>
 #include <libyul/optimiser/Suite.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 
 #include <libyul/backends/evm/EVMDialect.h>
 

test/yulPhaser/Chromosome.cpp

@@ -138,7 +138,7 @@ BOOST_AUTO_TEST_CASE(output_operator_should_create_concise_and_unambiguous_strin
 
 	BOOST_TEST(chromosome.length() == allSteps.size());
 	BOOST_TEST(chromosome.optimisationSteps() == allSteps);
-	BOOST_TEST(toString(chromosome) == "flcCUnDEvejsxIOoighFTLMRmVatrpuSd");
+	BOOST_TEST(toString(chromosome) == "flcCUnDEvejsxIOoighFTLMmVatrpuSd");
 }
 
 BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names)