Disallow optimizer steps that require SMT if none is available.

libyul/optimiser/OptimiserStep.h

@@ -20,6 +20,7 @@
 
 #include <libyul/Exceptions.h>
 
+#include <optional>
 #include <string>
 #include <set>
 
@@ -49,17 +50,41 @@ struct OptimiserStep
 	virtual ~OptimiserStep() = default;
 
 	virtual void run(OptimiserStepContext&, Block&) const = 0;
+	/// @returns non-nullopt if the step cannot be run, for example because it requires
+	/// an SMT solver to be loaded, but none is available. In that case, the string
+	/// contains a human-readable reason.
+	virtual std::optional<std::string> invalidInCurrentEnvironment() const = 0;
 	std::string name;
 };
 
 template <class Step>
 struct OptimiserStepInstance: public OptimiserStep
 {
+private:
+	template<typename T>
+	struct HasInvalidInCurrentEnvironmentMethod
+	{
+	private:
+		template<typename U> static auto test(int) -> decltype(U::invalidInCurrentEnvironment(), std::true_type());
+		template<typename> static std::false_type test(...);
+
+	public:
+		static constexpr bool value = decltype(test<T>(0))::value;
+	};
+
+public:
 	OptimiserStepInstance(): OptimiserStep{Step::name} {}
 	void run(OptimiserStepContext& _context, Block& _ast) const override
 	{
 		Step::run(_context, _ast);
 	}
+	std::optional<std::string> invalidInCurrentEnvironment() const override
+	{
+		if constexpr (HasInvalidInCurrentEnvironmentMethod<Step>::value)
+			return Step::invalidInCurrentEnvironment();
+		else
+			return std::nullopt;
+	};
 };
 
 

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -46,6 +46,15 @@ void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _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)
 {
 	if (_varDecl.variables.size() != 1 || !_varDecl.value)

libyul/optimiser/ReasoningBasedSimplifier.h

@@ -51,6 +51,7 @@ class ReasoningBasedSimplifier: public ASTModifier
 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;

libyul/optimiser/Suite.cpp

@@ -269,6 +269,7 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations)
 			insideLoop = false;
 			break;
 		default:
+		{
 			yulAssert(
 				string(NonStepAbbreviations).find(abbreviation) == string::npos,
 				"Unhandled syntactic element in the abbreviation sequence"
@@ -278,6 +279,14 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations)
 				OptimizerException,
 				"'"s + abbreviation + "' is not a valid step abbreviation"
 			);
+			optional<string> invalid = allSteps().at(stepAbbreviationToNameMap().at(abbreviation))->invalidInCurrentEnvironment();
+			assertThrow(
+				!invalid.has_value(),
+				OptimizerException,
+				"'"s + abbreviation + "' is invalid in the current environment: " + *invalid
+			);
+
+		}
 		}
 	assertThrow(!insideLoop, OptimizerException, "Unbalanced brackets");
 }