Value Constraint Based Simplifier.

libdevcore/Common.h

@@ -91,6 +91,24 @@ inline u256 s2u(s256 _u)
 		return u256(c_end + _u);
 }
 
+/// @returns the highest bit set in @a. If _v is zero, returns -1.
+inline int highestBitSet(u256 const& _v)
+{
+	if (_v == 0)
+		return -1;
+	else
+		return boost::multiprecision::msb(_v);
+}
+
+/// @returns the lowest bit set in @a. If _v is zero, returns 256
+inline int lowestBitSet(u256 const& _v)
+{
+	if (_v == 0)
+		return 256;
+	else
+		return boost::multiprecision::lsb(_v);
+}
+
 inline std::ostream& operator<<(std::ostream& os, bytes const& _bytes)
 {
 	std::ostringstream ss;

libyul/CMakeLists.txt

@@ -108,6 +108,8 @@ add_library(yul
 	optimiser/SyntacticalEquality.h
 	optimiser/UnusedPruner.cpp
 	optimiser/UnusedPruner.h
+	optimiser/ValueConstraintBasedSimplifier.cpp
+	optimiser/ValueConstraintBasedSimplifier.h
 	optimiser/VarDeclInitializer.cpp
 	optimiser/VarDeclInitializer.h
 	optimiser/VarNameCleaner.cpp

libyul/optimiser/DataFlowAnalyzer.cpp

@@ -213,6 +213,8 @@ void DataFlowAnalyzer::clearValues(set<YulString> _variables)
 			m_referencedBy[ref].erase(name);
 		m_references[name].clear();
 	}
+
+	valuesCleared(_variables);
 }
 
 bool DataFlowAnalyzer::inScope(YulString _variableName) const

libyul/optimiser/DataFlowAnalyzer.h

@@ -57,7 +57,7 @@ public:
 
 protected:
 	/// Registers the assignment.
-	void handleAssignment(std::set<YulString> const& _names, Expression* _value);
+	virtual void handleAssignment(std::set<YulString> const& _names, Expression* _value);
 
 	/// Creates a new inner scope.
 	void pushScope(bool _functionScope);
@@ -69,6 +69,10 @@ protected:
 	/// for example at points where control flow is merged.
 	void clearValues(std::set<YulString> _names);
 
+	/// Called whenever the variables given have been cleared, just before
+	/// some of them are assigned new values.
+	virtual void valuesCleared(std::set<YulString> const& /*_names*/) {}
+
 	/// Returns true iff the variable is in scope.
 	bool inScope(YulString _variableName) const;
 

libyul/optimiser/Suite.cpp

@@ -34,6 +34,7 @@
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionSimplifier.h>
+#include <libyul/optimiser/ValueConstraintBasedSimplifier.h>
 #include <libyul/optimiser/CommonSubexpressionEliminator.h>
 #include <libyul/optimiser/SSAReverser.h>
 #include <libyul/optimiser/SSATransform.h>
@@ -99,6 +100,7 @@ void OptimiserSuite::run(
 			RedundantAssignEliminator::run(*_dialect, ast);
 			RedundantAssignEliminator::run(*_dialect, ast);
 
+			ValueConstraintBasedSimplifier::run(*_dialect, ast);
 			ExpressionSimplifier::run(*_dialect, ast);
 			CommonSubexpressionEliminator{*_dialect}(ast);
 		}
@@ -156,6 +158,9 @@ void OptimiserSuite::run(
 			RedundantAssignEliminator::run(*_dialect, ast);
 			RedundantAssignEliminator::run(*_dialect, ast);
 			ExpressionSimplifier::run(*_dialect, ast);
+			ValueConstraintBasedSimplifier::run(*_dialect, ast);
+			ExpressionSimplifier::run(*_dialect, ast);
+			ValueConstraintBasedSimplifier::run(*_dialect, ast);
 			StructuralSimplifier{*_dialect}(ast);
 			BlockFlattener{}(ast);
 			CommonSubexpressionEliminator{*_dialect}(ast);

libyul/optimiser/ValueConstraintBasedSimplifier.cpp

@@ -0,0 +1,384 @@
+/*
+	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/>.
+*/
+/**
+ * Optimiser component that uses the simplification rules to simplify expressions.
+ */
+
+#include <libyul/optimiser/ValueConstraintBasedSimplifier.h>
+
+#include <libyul/optimiser/Semantics.h>
+
+#include <libyul/AsmData.h>
+#include <libyul/Utilities.h>
+#include <libyul/Exceptions.h>
+
+#include <libdevcore/CommonData.h>
+
+using namespace std;
+using namespace dev;
+using namespace yul;
+using namespace dev::solidity;
+
+namespace
+{
+class ConstraintDeduction: public boost::static_visitor<ValueConstraint>
+{
+public:
+	explicit ConstraintDeduction(map<YulString, ValueConstraint> const& _variableConstraints):
+		m_variableConstraints{_variableConstraints}
+	{}
+
+	ValueConstraint visit(Expression const& _expr)
+	{
+		return boost::apply_visitor(*this, _expr);
+	}
+
+	ValueConstraint operator()(Literal const& _literal)
+	{
+		return ValueConstraint::constant(valueOfLiteral(_literal));
+	}
+
+	ValueConstraint operator()(Identifier const& _identifier)
+	{
+		auto it = m_variableConstraints.find(_identifier.name);
+		if (it != m_variableConstraints.end())
+			return it->second;
+		else
+			return ValueConstraint{};
+	}
+
+	ValueConstraint operator()(FunctionCall const&)
+	{
+		return {};
+	}
+
+	ValueConstraint operator()(FunctionalInstruction const& _instr)
+	{
+		vector<Expression> const& args = _instr.arguments;
+		switch (_instr.instruction)
+		{
+		case dev::solidity::Instruction::ADD:
+			return visit(args.at(0)) + visit(args.at(1));
+		// TODO MUL
+		case dev::solidity::Instruction::SUB:
+			return visit(args.at(0)) - visit(args.at(1));
+		// TODO DIV, SDIV, MOD, SMOD, ADDMOD, MULMOD, EXP, SIGNEXTEND
+		case dev::solidity::Instruction::LT:
+			return visit(args.at(0)) < visit(args.at(1));
+		case dev::solidity::Instruction::GT:
+			return visit(args.at(1)) < visit(args.at(0));
+		// TODO SLT, SGT
+		case dev::solidity::Instruction::EQ:
+			return visit(args.at(1)) == visit(args.at(0));
+		case dev::solidity::Instruction::ISZERO:
+			return visit(args.at(0)) == ValueConstraint::constant(0);
+		case dev::solidity::Instruction::AND:
+			return visit(args.at(0)) & visit(args.at(1));
+		case dev::solidity::Instruction::OR:
+			return visit(args.at(0)) | visit(args.at(1));
+		// TODO XOR
+		case dev::solidity::Instruction::NOT:
+			return ~visit(args.at(0));
+		case dev::solidity::Instruction::BYTE:
+			// TODO Could be more specific.
+			return ValueConstraint::bitRange(7, 0);
+		case dev::solidity::Instruction::SHL:
+			return visit(args.at(1)) << visit(args.at(0));
+		case dev::solidity::Instruction::SHR:
+			return visit(args.at(1)) >> visit(args.at(0));
+		// TODO SAR
+		case dev::solidity::Instruction::ADDRESS:
+		case dev::solidity::Instruction::ORIGIN:
+		case dev::solidity::Instruction::CALLER:
+		case dev::solidity::Instruction::COINBASE:
+		case dev::solidity::Instruction::CREATE:
+		case dev::solidity::Instruction::CREATE2:
+			return ValueConstraint::bitRange(160, 0);
+
+		case dev::solidity::Instruction::CALL:
+		case dev::solidity::Instruction::CALLCODE:
+		case dev::solidity::Instruction::DELEGATECALL:
+		case dev::solidity::Instruction::STATICCALL:
+			return ValueConstraint::boolean();
+
+		case dev::solidity::Instruction::KECCAK256:
+		case dev::solidity::Instruction::EXTCODEHASH:
+		case dev::solidity::Instruction::BLOCKHASH:
+		case dev::solidity::Instruction::MLOAD:
+		case dev::solidity::Instruction::SLOAD:
+
+		// These could be restricted in a real-world setting:
+		case dev::solidity::Instruction::BALANCE:
+		case dev::solidity::Instruction::CALLVALUE:
+		case dev::solidity::Instruction::CALLDATASIZE:
+		case dev::solidity::Instruction::GASPRICE:
+		case dev::solidity::Instruction::EXTCODESIZE:
+		case dev::solidity::Instruction::RETURNDATASIZE:
+		case dev::solidity::Instruction::TIMESTAMP:
+		case dev::solidity::Instruction::NUMBER:
+		case dev::solidity::Instruction::DIFFICULTY:
+		case dev::solidity::Instruction::GASLIMIT:
+		case dev::solidity::Instruction::PC:
+		case dev::solidity::Instruction::MSIZE:
+		case dev::solidity::Instruction::GAS:
+		default:
+			return {};
+		}
+	}
+
+private:
+
+	map<YulString, ValueConstraint> const& m_variableConstraints;
+};
+}
+
+ValueConstraint ValueConstraint::constant(u256 const& _value)
+{
+	return ValueConstraint{_value, _value, _value, _value};
+}
+
+ValueConstraint ValueConstraint::boolean()
+{
+	return ValueConstraint{0, 1, 0, 1};
+}
+
+ValueConstraint ValueConstraint::bitRange(size_t _highest, size_t _lowest)
+{
+	yulAssert(_highest >= _lowest, "");
+	return valueFromBits(
+		0,
+		(u256(-1) >> (255 - _highest)) & ~(u256(-1) >> (256 - _lowest))
+	);
+}
+
+ValueConstraint ValueConstraint::valueFromBits(u256 _minBits, u256 _maxBits)
+{
+	int highestBit = highestBitSet(_maxBits);
+	return ValueConstraint{
+		0,
+		u256(-1) >> (255 - highestBit),
+		move(_minBits),
+		move(_maxBits)
+	};
+}
+
+ValueConstraint ValueConstraint::bitsFromValue(u256 _minValue, u256 _maxValue)
+{
+	int highestBit = highestBitSet(_maxValue);
+	return ValueConstraint{
+		move(_minValue),
+		move(_maxValue),
+		0,
+		u256(-1) >> (255 - highestBit)
+	};
+}
+
+ValueConstraint ValueConstraint::operator&(ValueConstraint const& _other)
+{
+	return valueFromBits(
+		minBits & _other.minBits,
+		maxBits & _other.maxBits
+	);
+}
+
+ValueConstraint ValueConstraint::operator|(ValueConstraint const& _other)
+{
+	return valueFromBits(
+		minBits | _other.minBits,
+		maxBits | _other.maxBits
+	);
+}
+
+ValueConstraint ValueConstraint::operator~()
+{
+	return valueFromBits(~maxBits, ~minBits);
+}
+
+ValueConstraint ValueConstraint::operator+(ValueConstraint const& _other)
+{
+	if (bigint(maxValue) + bigint(_other.maxValue) > u256(-1))
+		return ValueConstraint{}; // overflow
+	else
+		return bitsFromValue(
+			minValue + _other.minValue,
+			maxValue + _other.maxValue
+		);
+}
+
+ValueConstraint ValueConstraint::operator-(ValueConstraint const& _other)
+{
+	if (minValue < _other.maxValue)
+		return ValueConstraint{}; // underflow
+	else
+		return bitsFromValue(
+			maxValue - _other.minValue,
+			minValue - _other.maxValue
+		);
+}
+
+ValueConstraint ValueConstraint::operator<(ValueConstraint const& _other)
+{
+	if (maxValue < _other.minValue)
+		return constant(1);
+	else if (minValue >= _other.maxValue)
+		return constant(0);
+	else
+		return boolean();
+}
+
+ValueConstraint ValueConstraint::operator==(ValueConstraint const& _other)
+{
+	if (minValue == maxValue && minValue == _other.minValue && _other.minValue == _other.maxValue)
+		return constant(1);
+	else if (minBits == maxBits && minBits == _other.maxBits && _other.minBits == _other.maxBits)
+		return constant(1);
+	else if (maxValue < _other.minValue || minValue > _other.maxValue)
+		return constant(0);
+	else if ((maxBits == 0 && _other.minBits == 1) || (minBits == 1 && _other.maxBits == 0))
+		return constant(0);
+	else
+		return boolean();
+}
+
+ValueConstraint ValueConstraint::operator<<(ValueConstraint const& _other)
+{
+	if (boost::optional<u256> c = _other.isConstant())
+	{
+		if (*c >= 256)
+			return constant(0);
+		unsigned amount = unsigned(*c);
+		return ValueConstraint{
+			dev::bigintShiftLeftWorkaround(minValue, amount),
+			dev::bigintShiftLeftWorkaround(maxValue, amount),
+			dev::bigintShiftLeftWorkaround(minBits, amount),
+			dev::bigintShiftLeftWorkaround(maxBits, amount)
+		};
+	}
+	else
+	{
+		size_t lowestBit = lowestBitSet(maxBits);
+		if (lowestBit + bigint(_other.minValue) > 255)
+			return constant(0);
+		else
+			/// TODO could be more accurate, also taking "lastBit set" and _other.maxValue into account.
+			return bitRange(255, lowestBit + size_t(_other.minValue));
+	}
+}
+
+ValueConstraint ValueConstraint::operator>>(ValueConstraint const& _other)
+{
+	if (boost::optional<u256> c = _other.isConstant())
+	{
+		if (*c >= 256)
+			return constant(0);
+		unsigned amount = unsigned(*c);
+		return ValueConstraint{
+			minValue >> amount,
+			maxValue >> amount,
+			minBits >> amount,
+			maxBits >> amount
+		};
+	}
+	else
+	{
+		int highestBit = highestBitSet(maxBits);
+		if (highestBit - bigint(_other.minValue) < 0)
+			return constant(0);
+		else
+			/// TODO could be more accurate, also taking "lastBit set" and _other.maxValue into account.
+			return bitRange(size_t(highestBit - _other.minValue), 0);
+	}
+}
+
+boost::optional<u256> ValueConstraint::isConstant() const
+{
+	if (minValue == maxValue)
+		return minValue;
+	else
+		return {};
+}
+
+void ValueConstraintBasedSimplifier::visit(Expression& _expression)
+{
+	ASTModifier::visit(_expression);
+
+	// TODO this runs constraint deduction multiple times on the same sub-expression.
+
+	// Replace movable expressions that are equal to constants by constants.
+	if (_expression.type() != typeid(Literal) && MovableChecker(m_dialect, _expression).movable())
+	{
+		ValueConstraint c = ConstraintDeduction{m_variableConstraints}.visit(_expression);
+		if (boost::optional<u256> value = c.isConstant())
+			_expression = Literal{
+				locationOf(_expression),
+				LiteralKind::Number,
+				YulString{formatNumber(*value)},
+				{}
+			};
+	}
+
+
+	// TODO We need more complicated rules that also do things like
+	// and(x, 0xff) -> x if x is known to be less than 256
+	// These rules might be just rules from the ruleList,
+	// where the `feasible` function gets access to the value constraints.
+	// It might also be a new RuleList that re-uses the existing classes.
+	// We could add another template to SimplificationRule to modify the
+	// parameter of the feasibility function, or we capture somehow.
+
+	// Another next step is to add new information in control-flow branches.
+	// If such a branch is terminating, also the 'else' branch can
+	// get new information.
+
+	// Finally, the ValueConstrainst should be extended such that the upper
+	// and lower bounds can be other variables.
+}
+
+void ValueConstraintBasedSimplifier::run(Dialect const& _dialect, Block& _ast)
+{
+	ValueConstraintBasedSimplifier{_dialect}(_ast);
+}
+
+void ValueConstraintBasedSimplifier::handleAssignment(set<YulString> const& _names, Expression* _value)
+{
+	// Determine the constraint before the assignment is performed, because
+	// that will change the values of variables.
+
+	ValueConstraint constraint = ValueConstraint::constant(0);
+	if (_value)
+		constraint = ConstraintDeduction{m_variableConstraints}.visit(*_value);
+
+	// This calls valuesCleared internally, which might clear more values
+	// than just _names.
+	DataFlowAnalyzer::handleAssignment(_names, _value);
+
+	if (_value)
+	{
+		if (_names.size() == 1)
+			m_variableConstraints[*_names.begin()] = constraint;
+	}
+	else
+		for (auto const& name: _names)
+			m_variableConstraints[name] = constraint;
+}
+
+void ValueConstraintBasedSimplifier::valuesCleared(set<YulString> const& _names)
+{
+	for (auto const& name: _names)
+		m_variableConstraints.erase(name);
+}
+

libyul/optimiser/ValueConstraintBasedSimplifier.h

@@ -0,0 +1,106 @@
+/*
+	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/>.
+*/
+/**
+ * Optimiser component that uses the simplification rules to simplify expressions.
+ */
+
+#pragma once
+
+#include <libyul/AsmDataForward.h>
+
+#include <libyul/optimiser/DataFlowAnalyzer.h>
+
+#include <libdevcore/Common.h>
+
+namespace yul
+{
+struct Dialect;
+
+struct ValueConstraint
+{
+	static ValueConstraint constant(dev::u256 const& _value);
+	static ValueConstraint boolean();
+	/// @returns a constraint that does not restrict the bits between
+	/// (inclusive) _highest and _lowest bit but forces all other
+	/// bits to zero.
+	static ValueConstraint bitRange(size_t _highest, size_t _lowest);
+
+	/// Fill the minValue and maxValue fields from the minBits and maxBits fields.
+	static ValueConstraint valueFromBits(dev::u256 _minBits, dev::u256 _maxBits);
+	/// Fill the minBits and maxBits fields from the minValue and maxValue fields.
+	static ValueConstraint bitsFromValue(dev::u256 _minValue, dev::u256 _maxValue);
+
+	ValueConstraint operator&(ValueConstraint const& _other);
+	ValueConstraint operator|(ValueConstraint const& _other);
+	ValueConstraint operator~();
+	ValueConstraint operator+(ValueConstraint const& _other);
+	ValueConstraint operator-(ValueConstraint const& _other);
+	ValueConstraint operator<(ValueConstraint const& _other);
+	ValueConstraint operator==(ValueConstraint const& _other);
+	ValueConstraint operator<<(ValueConstraint const& _other);
+	ValueConstraint operator>>(ValueConstraint const& _other);
+
+	boost::optional<dev::u256> isConstant() const;
+
+	dev::u256 minValue = 0;
+	dev::u256 maxValue = dev::u256(-1);
+	dev::u256 minBits = 0; ///< For each 1-bit here, the value's bit is also 1
+	dev::u256 maxBits = dev::u256(-1); ///< For each 0-bit here, the value's bit is also 0
+};
+
+/**
+ * Performs simplifications that take value and bit constraints
+ * of variables and expressions into account.
+ *
+ * Example:
+ *
+ * let x := and(callvalue(), 0xff)
+ * if lt(x, 0x100) { ... }
+ *
+ * is reduced to
+ *
+ * let x := and(callvalue(), 0xff)
+ * if 1 { ... }
+ *
+ * because ``x`` is known to be at most 0xff.
+ *
+ * Most effective if run on code in SSA form.
+ *
+ * Prerequisite: Disambiguator.
+ */
+class ValueConstraintBasedSimplifier: public DataFlowAnalyzer
+{
+public:
+	using ASTModifier::operator();
+
+	void visit(Expression& _expression) override;
+
+	static void run(Dialect const& _dialect, Block& _ast);
+
+protected:
+	void handleAssignment(std::set<YulString> const& _names, Expression* _value) override;
+
+	void valuesCleared(std::set<YulString> const& _names) override;
+
+private:
+	explicit ValueConstraintBasedSimplifier(Dialect const& _dialect): DataFlowAnalyzer(_dialect) {}
+
+	std::map<YulString, ValueConstraint> m_variableConstraints;
+	ValueConstraint m_currentConstraint;
+};
+
+}

test/libyul/YulOptimizerTest.cpp

@@ -35,6 +35,7 @@
 #include <libyul/optimiser/MainFunction.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/ExpressionSimplifier.h>
+#include <libyul/optimiser/ValueConstraintBasedSimplifier.h>
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionJoiner.h>
 #include <libyul/optimiser/SSAReverser.h>
@@ -182,6 +183,11 @@ bool YulOptimizerTest::run(ostream& _stream, string const& _linePrefix, bool con
 		disambiguate();
 		ExpressionSimplifier::run(*m_dialect, *m_ast);
 	}
+	else if (m_optimizerStep == "valueConstraintBasedSimplifier")
+	{
+		disambiguate();
+		ValueConstraintBasedSimplifier::run(*m_dialect, *m_ast);
+	}
 	else if (m_optimizerStep == "fullSimplify")
 	{
 		disambiguate();

test/libyul/yulOptimizerTests/valueConstraintBasedSimplifier/lt.yul

@@ -0,0 +1,38 @@
+{
+    let x := 2
+    if lt(x, 9) { sstore(0, 1) }
+    if lt(x, 2) { sstore(0, 1) }
+    if gt(x, 0) { sstore(0, 1) }
+    if lt(9, x) { sstore(0, 1) }
+    if lt(2, x) { sstore(0, 1) }
+    if gt(0, x) { sstore(0, 1) }
+}
+// ----
+// valueConstraintBasedSimplifier
+// {
+//     let x := 2
+//     if 1
+//     {
+//         sstore(0, 1)
+//     }
+//     if 0
+//     {
+//         sstore(0, 1)
+//     }
+//     if 1
+//     {
+//         sstore(0, 1)
+//     }
+//     if 0
+//     {
+//         sstore(0, 1)
+//     }
+//     if 0
+//     {
+//         sstore(0, 1)
+//     }
+//     if 0
+//     {
+//         sstore(0, 1)
+//     }
+// }

test/libyul/yulOptimizerTests/valueConstraintBasedSimplifier/lt_bits_combined.yul

@@ -0,0 +1,18 @@
+{
+    let x := and(callvalue(), 0xff)
+    if lt(x, 0x100) { sstore(0, 1) }
+    if lt(x, 0xff) { sstore(0, 1) }
+}
+// ----
+// valueConstraintBasedSimplifier
+// {
+//     let x := and(callvalue(), 0xff)
+//     if 1
+//     {
+//         sstore(0, 1)
+//     }
+//     if lt(x, 0xff)
+//     {
+//         sstore(0, 1)
+//     }
+// }

test/libyul/yulOptimizerTests/valueConstraintBasedSimplifier/smoke.yul

@@ -0,0 +1,6 @@
+{
+}
+// ----
+// valueConstraintBasedSimplifier
+// {
+// }

test/tools/yulopti.cpp

@@ -43,6 +43,7 @@
 #include <libyul/optimiser/MainFunction.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/ExpressionSimplifier.h>
+#include <libyul/optimiser/ValueConstraintBasedSimplifier.h>
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionJoiner.h>
 #include <libyul/optimiser/RedundantAssignEliminator.h>
@@ -129,10 +130,10 @@ public:
 				disambiguated = true;
 			}
 			cout << "(q)quit/(f)flatten/(c)se/initialize var(d)ecls/(x)plit/(j)oin/(g)rouper/(h)oister/" << endl;
-			cout << "  (e)xpr inline/(i)nline/(s)implify/varname c(l)eaner/(u)nusedprune/ss(a) transform/" << endl;
+			cout << "  (e)xpr inline/(i)nline/(s)implify/(C)onstraint simplify/varname c(l)eaner/" << endl;
-			cout << "  (r)edundant assign elim./re(m)aterializer/f(o)r-loop-pre-rewriter/" << endl;
+			cout << "  (u)nusedprune/ss(a) transform/(r)edundant assign elim./re(m)aterializer/" << endl;
-			cout << "  s(t)ructural simplifier/equi(v)alent function combiner/ssa re(V)erser/? " << endl;
+			cout << "  f(o)r-loop-pre-rewriter/s(t)ructural simplifier/equi(v)alent function combiner/" << endl;
-			cout << "  stack com(p)ressor? " << endl;
+			cout << "  ssa re(V)erser/stack com(p)ressor? " << endl;
 			cout.flush();
 			int option = readStandardInputChar();
 			cout << ' ' << char(option) << endl;
@@ -176,6 +177,9 @@ public:
 			case 's':
 				ExpressionSimplifier::run(*m_dialect, *m_ast);
 				break;
+			case 'C':
+				ValueConstraintBasedSimplifier::run(*m_dialect, *m_ast);
+				break;
 			case 't':
 				(StructuralSimplifier{*m_dialect})(*m_ast);
 				break;