implemert strict comparisons

libsolutil/BooleanLP.cpp

@@ -342,7 +342,7 @@ void BooleanLPSolver::addLetBindings(Expression const& _let, map<string, size_t>
 		bool isBool = binding.arguments.at(0).sort->kind == Kind::Bool;
 		Expression var = declareInternalVariable(isBool);
 		newBindings.insert({binding.name, state().variables.at(var.name)});
-		addAssertion(var == binding.arguments.at(0));
+		addAssertion(var == binding.arguments.at(0), _letBindings);
 	}
 	for (auto&& [name, varIndex]: newBindings)
 		_letBindings.insert({name, varIndex});
@@ -429,6 +429,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
 		}
 		else
 		{
+			// TODO We can only do this if we know it is an integer!
 			// X > b
 			// -x < -b
 			// -x <= -b - 1

libsolutil/LP.h

@@ -47,6 +47,56 @@ struct Constraint
 	bool operator==(Constraint const& _other) const;
 };
 
+/**
+ * A two-dimensional rational number "a + b*delta" that can be used to perform strict comparisons:
+ * x > 0 is transformed into x >= 1*delta, where delta is assumed to be "small". Its value
+ * is never explicitly computed / set, it is just a symbolic parameter.
+ */
+class RationalWithDelta
+{
+public:
+	RationalWithDelta(rational _x): m_main(move(_x)) {}
+	static RationalWithDelta delta()
+	{
+		RationalWithDelta x(0);
+		x.m_delta = 1;
+		return x;
+	}
+
+	RationalWithDelta& operator+=(RationalWithDelta const& _other)
+	{
+		m_main += _other.m_main;
+		m_delta += _other.m_delta;
+		return *this;
+	}
+	RationalWithDelta& operator*=(rational const& _factor)
+	{
+		m_main *= _factor;
+		m_delta *= _factor;
+		return *this;
+	}
+	bool operator<=(RationalWithDelta const& _other)
+	{
+		return std::tie(m_main, m_delta) <= std::tie(_other.m_main, _other.m_delta);
+	}
+	bool operator<(RationalWithDelta const& _other)
+	{
+		return std::tie(m_main, m_delta) < std::tie(_other.m_main, _other.m_delta);
+	}
+	bool operator==(RationalWithDelta const& _other)
+	{
+		return std::tie(m_main, m_delta) == std::tie(_other.m_main, _other.m_delta);
+	}
+	bool operator!=(RationalWithDelta const& _other)
+	{
+		return std::tie(m_main, m_delta) != std::tie(_other.m_main, _other.m_delta);
+	}
+
+private:
+	rational m_main;
+	rational m_delta;
+};
+
 /**
  * State used when solving an LP problem.
  */

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -249,15 +249,19 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 		);
 		*/
 	case evmasm::Instruction::LT:
+		// TODO use x <= y - 1 directly?
 		return booleanValue(arguments.at(0) < arguments.at(1));
 	case evmasm::Instruction::SLT:
+		// TODO use x <= y - 1 directly?
 		return booleanValue(
 			twosComplementToUpscaledUnsigned(arguments.at(0)) + smtutil::Expression(bigint(1) << 256) <
 			twosComplementToUpscaledUnsigned(arguments.at(1)) + smtutil::Expression(bigint(1) << 256)
 		);
 	case evmasm::Instruction::GT:
+		// TODO use x >= y + 1 directly!
 		return booleanValue(arguments.at(0) > arguments.at(1));
 	case evmasm::Instruction::SGT:
+		// TODO use x >= y + 1 directly!
 		return booleanValue(
 			twosComplementToUpscaledUnsigned(arguments.at(0)) + smtutil::Expression(bigint(1) << 256) >
 			twosComplementToUpscaledUnsigned(arguments.at(1)) + smtutil::Expression(bigint(1) << 256)