Boolean LP Solver.

libsolutil/BooleanLP.cpp

@@ -0,0 +1,713 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolutil/BooleanLP.h>
+
+#include <libsolutil/CommonData.h>
+#include <libsolutil/StringUtils.h>
+#include <liblangutil/Exceptions.h>
+
+#include <libsolutil/RationalVectors.h>
+
+#include <range/v3/view/enumerate.hpp>
+#include <range/v3/view/transform.hpp>
+#include <range/v3/view/filter.hpp>
+#include <range/v3/view/tail.hpp>
+#include <range/v3/view/iota.hpp>
+#include <range/v3/algorithm/all_of.hpp>
+#include <range/v3/algorithm/any_of.hpp>
+#include <range/v3/algorithm/max.hpp>
+#include <range/v3/algorithm/count_if.hpp>
+#include <range/v3/iterator/operations.hpp>
+
+#include <boost/range/algorithm_ext/erase.hpp>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+using rational = boost::rational<bigint>;
+
+
+pair<bool, map<size_t, bool>> DPLL::simplify()
+{
+	// TODO use vector?
+	map<size_t, bool> assignments;
+	while (!clauses.empty() && !ranges::all_of(clauses, [](Clause const& _c) { return _c.literals.size() > 1; }))
+	{
+		// TODO this assumes that no clause contains more than one constraint
+		// TODO add an assertion for that.
+
+		for (Clause const& c: clauses)
+			if (c.literals.empty())
+				return {false, {}};
+			else if (c.literals.size() == 1)
+			{
+				Literal const& literal = c.literals.front();
+				if (literal.kind == Literal::Constraint)
+					constraints.push_back(literal.index);
+				else
+				{
+					bool value = literal.kind == Literal::PositiveVariable ? true : false;
+					if (assignments.count(literal.index) && assignments.at(literal.index) != value)
+						return {false, {}};
+					//cout << "Assigning" << variableName(literal.index) << " " << value << endl;
+					assignments[literal.index] = value;
+				}
+			}
+
+		if (!setVariables(assignments, true))
+			return {false, {}};
+	}
+	return {true, move(assignments)};
+}
+
+size_t DPLL::findUnassignedVariable() const
+{
+	for (Clause const& c: clauses)
+		for (Literal const& l: c.literals)
+			if (l.kind != Literal::Constraint)
+				return l.index;
+	solAssert(false, "");
+	return 0;
+}
+
+bool DPLL::setVariable(size_t _index, bool _value)
+{
+	return setVariables({{_index, _value}});
+}
+
+bool DPLL::setVariables(map<size_t, bool> const& _assignments, bool _removeSingleConstraintClauses)
+{
+	// TODO do this in a way so that we do not have to copy twice.
+	vector<Clause> prunedClauses;
+	for (Clause const& c: clauses)
+	{
+		bool skipClause = false;
+		vector<Literal> newClause;
+		if (_removeSingleConstraintClauses && c.literals.size() == 1 && c.literals.front().kind == Literal::Constraint)
+			continue;
+		for (Literal const& l: c.literals)
+			if (l.kind != Literal::Constraint && _assignments.count(l.index))
+			{
+				if (_assignments.at(l.index) == (l.kind == Literal::PositiveVariable))
+				{
+					skipClause = true;
+					break;
+				}
+			}
+			else
+				newClause.push_back(l);
+		if (skipClause)
+			continue;
+		if (newClause.empty())
+			return false;
+		prunedClauses.push_back(Clause{move(newClause)});
+	}
+	clauses = move(prunedClauses);
+	return true;
+}
+
+void BooleanLPSolver::reset()
+{
+	m_state = vector<State>{{State{}}};
+	m_internalVariableCounter = 0;
+	m_constraintCounter = 0;
+	// Do not reset the solver, it should retain its cache.
+}
+
+void BooleanLPSolver::push()
+{
+	if (m_state.back().infeasible)
+	{
+		m_state.emplace_back();
+		m_state.back().infeasible = true;
+		return;
+	}
+	map<string, size_t> variables = m_state.back().variables;
+	map<size_t, array<optional<boost::rational<bigint>>, 2>> bounds = m_state.back().bounds;
+	vector<bool> isBooleanVariable = m_state.back().isBooleanVariable;
+	m_state.emplace_back();
+	m_state.back().variables = move(variables);
+	m_state.back().isBooleanVariable = move(isBooleanVariable);
+	m_state.back().bounds = move(bounds);
+}
+
+void BooleanLPSolver::pop()
+{
+	m_state.pop_back();
+	solAssert(!m_state.empty(), "");
+}
+
+void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _sort)
+{
+	// Internal variables are '$<number>'
+	string name = (_name.empty() || _name.at(0) != '$') ? _name : "$$" + _name;
+	// TODO This will not be an integer variable in our model.
+	// Introduce a new kind?
+	solAssert(_sort && (_sort->kind == Kind::Int || _sort->kind == Kind::Bool), "");
+	solAssert(!m_state.back().variables.count(name), "");
+	declareVariable(name, _sort->kind == Kind::Bool);
+}
+
+void BooleanLPSolver::addAssertion(Expression const& _expr)
+{
+	if (_expr.arguments.empty())
+		m_state.back().clauses.emplace_back(Clause{vector<Literal>{*parseLiteral(_expr)}});
+	else if (_expr.name == "=")
+	{
+		// Try to see if both sides are linear.
+		optional<vector<rational>> left = parseLinearSum(_expr.arguments.at(0));
+		optional<vector<rational>> right = parseLinearSum(_expr.arguments.at(1));
+		if (left && right)
+		{
+			vector<rational> data = *left - *right;
+			data[0] *= -1;
+			Constraint c{move(data), _expr.name == "="};
+			if (!tryAddDirectBounds(c))
+			{
+				size_t index = addConstraint(move(c));
+				m_state.back().clauses.emplace_back(Clause{vector<Literal>{Literal{Literal::Constraint, index}}});
+			}
+		}
+		else if (_expr.arguments.at(0).arguments.empty() && isBooleanVariable(_expr.arguments.at(0).name))
+			addBooleanEquality(*parseLiteral(_expr.arguments.at(0)), _expr.arguments.at(1));
+		else if (_expr.arguments.at(1).arguments.empty() && isBooleanVariable(_expr.arguments.at(1).name))
+			addBooleanEquality(*parseLiteral(_expr.arguments.at(1)), _expr.arguments.at(0));
+		else
+		{
+			Literal newBoolean = *parseLiteral(declareInternalBoolean());
+			addBooleanEquality(newBoolean, _expr.arguments.at(0));
+			addBooleanEquality(newBoolean, _expr.arguments.at(1));
+		}
+	}
+	else if (_expr.name == "and")
+	{
+		addAssertion(_expr.arguments.at(0));
+		addAssertion(_expr.arguments.at(1));
+	}
+	else if (_expr.name == "or")
+	{
+		// We could try to parse a full clause here.
+		Literal left = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0));
+		Literal right = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(1));
+		if (left.kind == Literal::Constraint && right.kind == Literal::Constraint)
+		{
+			// We cannot have more than one constraint per clause.
+			right = *parseLiteral(declareInternalBoolean());
+			addBooleanEquality(right, _expr.arguments.at(1));
+		}
+		m_state.back().clauses.emplace_back(Clause{vector<Literal>{left, right}});
+	}
+	else if (_expr.name == "not")
+	{
+		Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));
+		m_state.back().clauses.emplace_back(Clause{vector<Literal>{l}});
+	}
+	else if (_expr.name == "<=")
+	{
+		optional<vector<rational>> left = parseLinearSum(_expr.arguments.at(0));
+		optional<vector<rational>> right = parseLinearSum(_expr.arguments.at(1));
+		if (!left || !right)
+			return;
+
+		vector<rational> data = *left - *right;
+		data[0] *= -1;
+		Constraint c{move(data), _expr.name == "="};
+		if (!tryAddDirectBounds(c))
+		{
+			size_t index = addConstraint(move(c));
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{Literal{Literal::Constraint, index}}});
+		}
+	}
+	else if (_expr.name == ">=")
+		addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0));
+	else if (_expr.name == "<")
+		addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1);
+	else if (_expr.name == ">")
+		addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0));
+}
+
+
+pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	cout << "Solving boolean constraint system" << endl;
+	cout << toString() << endl;
+
+	if (m_state.back().infeasible)
+		return make_pair(CheckResult::UNSATISFIABLE, vector<string>{});
+
+	// TODO compress variables because we ignore boolean variables
+	SolvingState state;
+	for (auto&& [name, index]: m_state.back().variables)
+		resizeAndSet(state.variableNames, index, name);
+	for (auto&& [index, value]: m_state.back().bounds)
+		resizeAndSet(state.bounds, index, value);
+
+	std::vector<Clause> clauses;
+	for (State const& s: m_state)
+		for (Clause const& clause: s.clauses)
+			clauses.push_back(clause);
+
+	auto&& [result, model] = runDPLL(state, DPLL{move(clauses), {}});
+	if (result == CheckResult::SATISFIABLE)
+	{
+		vector<string> requestedModel;
+		for (Expression const& e: _expressionsToEvaluate)
+			requestedModel.emplace_back(
+				e.arguments.empty() && model.count(e.name) ?
+				::toString(model[e.name], 0) :
+				string("unknown")
+			);
+		return {result, move(requestedModel)};
+	}
+	else
+		return {result, {}};
+}
+
+string BooleanLPSolver::toString() const
+{
+	string result;
+
+	for (State const& s: m_state)
+		for (Clause const& c: s.clauses)
+			result += toString(c);
+	result += "-- Bounds:\n";
+	for (State const& s: m_state)
+		for (auto&& [index, bounds]: s.bounds)
+		{
+			if (!bounds[0] && !bounds[1])
+				continue;
+			if (bounds[0])
+				result += ::toString(*bounds[0]) + " <= ";
+			result += variableName(index);
+			if (bounds[1])
+				result += " <= " + ::toString(*bounds[1]);
+			result += "\n";
+		}
+	return result;
+}
+
+Expression BooleanLPSolver::declareInternalBoolean()
+{
+	string name = "$" + to_string(m_internalVariableCounter++);
+	declareVariable(name, true);
+	return smtutil::Expression(name, {}, SortProvider::boolSort);
+}
+
+void BooleanLPSolver::declareVariable(string const& _name, bool _boolean)
+{
+	size_t index = m_state.back().variables.size() + 1;
+	m_state.back().variables[_name] = index;
+	resizeAndSet(m_state.back().isBooleanVariable, index, _boolean);
+}
+
+optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr)
+{
+	// TODO constanst true/false?
+
+	if (_expr.arguments.empty())
+	{
+		if (isBooleanVariable(_expr.name))
+			return Literal{
+				Literal::PositiveVariable,
+				m_state.back().variables.at(_expr.name)
+			};
+	}
+	else if (_expr.name == "not")
+		return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));
+	else if (_expr.name == "<=")
+	{
+		optional<vector<rational>> left = parseLinearSum(_expr.arguments.at(0));
+		optional<vector<rational>> right = parseLinearSum(_expr.arguments.at(1));
+		if (!left || !right)
+			return {};
+
+		vector<rational> data = *left - *right;
+		data[0] *= -1;
+
+		return Literal{Literal::Constraint, addConstraint(Constraint{move(data), false})};
+	}
+	else if (_expr.name == ">=")
+		return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0));
+	else if (_expr.name == "<")
+		return parseLiteral(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1);
+	else if (_expr.name == ">")
+		return parseLiteral(_expr.arguments.at(1) < _expr.arguments.at(0));
+
+	return {};
+}
+
+Literal BooleanLPSolver::negate(Literal const& _lit)
+{
+	switch (_lit.kind)
+	{
+	case Literal::NegativeVariable:
+		return Literal{Literal::PositiveVariable, _lit.index};
+	case Literal::PositiveVariable:
+		return Literal{Literal::NegativeVariable, _lit.index};
+	default:
+		break;
+	}
+
+	Constraint const& c = constraint(_lit.index);
+
+	solAssert(!c.equality, "");
+
+	// X > b
+	// -x < -b
+	// -x <= -b - 1
+
+	Constraint negated = c;
+	negated.data *= -1;
+	negated.data[0] -= 1;
+
+	return Literal{Literal::Constraint, addConstraint(move(negated))};
+}
+
+Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr)
+{
+	if (optional<Literal> literal = parseLiteral(_expr))
+		return *literal;
+	else
+	{
+		Literal newBoolean = *parseLiteral(declareInternalBoolean());
+		addBooleanEquality(newBoolean, _expr);
+		return newBoolean;
+	}
+}
+
+optional<vector<rational>> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr) const
+{
+	if (_expr.arguments.empty() || _expr.name == "*")
+		return parseProduct(_expr);
+	else if (_expr.name == "+" || _expr.name == "-")
+	{
+		optional<vector<rational>> left = parseLinearSum(_expr.arguments.at(0));
+		optional<vector<rational>> right = parseLinearSum(_expr.arguments.at(1));
+		if (!left || !right)
+			return std::nullopt;
+		return _expr.name == "+" ? add(*left, *right) : *left - *right;
+	}
+	else
+		return std::nullopt;
+}
+
+optional<vector<rational>> BooleanLPSolver::parseProduct(smtutil::Expression const& _expr) const
+{
+	if (_expr.arguments.empty())
+		return parseFactor(_expr);
+	else if (_expr.name == "*")
+		// The multiplication ensures that only one of them can be a variable.
+		return vectorProduct(parseFactor(_expr.arguments.at(0)), parseFactor(_expr.arguments.at(1)));
+	else
+		return std::nullopt;
+}
+
+optional<vector<rational>> BooleanLPSolver::parseFactor(smtutil::Expression const& _expr) const
+{
+	solAssert(_expr.arguments.empty(), "");
+	solAssert(!_expr.name.empty(), "");
+	if ('0' <= _expr.name[0] && _expr.name[0] <= '9')
+		return vector<rational>{rational(bigint(_expr.name))};
+	else if (_expr.name == "true")
+		return vector<rational>{rational(bigint(1))};
+	else if (_expr.name == "false")
+		return vector<rational>{rational(bigint(0))};
+
+	size_t index = m_state.back().variables.at(_expr.name);
+	solAssert(index > 0, "");
+	if (isBooleanVariable(index))
+		return nullopt;
+	return factorForVariable(index, rational(bigint(1)));
+}
+
+bool BooleanLPSolver::tryAddDirectBounds(Constraint const& _constraint)
+{
+	auto nonzero = _constraint.data | ranges::views::enumerate | ranges::views::tail | ranges::views::filter(
+		[](std::pair<size_t, rational> const& _x) { return !!_x.second; }
+	);
+	// TODO we can exit early on in the loop above.
+	if (ranges::distance(nonzero) > 1)
+		return false;
+
+	//cout << "adding direct bound." << endl;
+	if (ranges::distance(nonzero) == 0)
+	{
+		// 0 <= b or 0 = b
+		if (
+			_constraint.data.front() < 0 ||
+			(_constraint.equality && _constraint.data.front() != 0)
+		)
+		{
+//			cout << "SETTING INF" << endl;
+			m_state.back().infeasible = true;
+		}
+	}
+	else
+	{
+		auto&& [varIndex, factor] = nonzero.front();
+		// a * x <= b
+		rational bound = _constraint.data[0] / factor;
+		if (factor > 0 || _constraint.equality)
+			addUpperBound(varIndex, bound);
+		if (factor < 0 || _constraint.equality)
+			addLowerBound(varIndex, bound);
+	}
+	return true;
+}
+
+void BooleanLPSolver::addUpperBound(size_t _index, rational _value)
+{
+	//cout << "adding " << variableName(_index) << " <= " << toString(_value) << endl;
+	if (!m_state.back().bounds[_index][1] || _value < *m_state.back().bounds[_index][1])
+		m_state.back().bounds[_index][1] = move(_value);
+}
+
+void BooleanLPSolver::addLowerBound(size_t _index, rational _value)
+{
+	// Lower bound must be at least zero.
+	_value = max(_value, rational{});
+	//cout << "adding " << variableName(_index) << " >= " << toString(_value) << endl;
+	if (!m_state.back().bounds[_index][0] || _value > *m_state.back().bounds[_index][0])
+		m_state.back().bounds[_index][0] = move(_value);
+}
+
+size_t BooleanLPSolver::addConstraint(Constraint _constraint)
+{
+	size_t index = ++m_constraintCounter;
+	m_state.back().constraints[index] = move(_constraint);
+	return index;
+}
+
+void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expression const& _right)
+{
+	if (optional<Literal> right = parseLiteral(_right))
+	{
+		// includes: not, <=, <, >=, >, boolean variables.
+		// a = b <=> (-a \/ b) /\ (a \/ -b)
+		Literal negLeft = negate(_left);
+		Literal negRight = negate(*right);
+		m_state.back().clauses.emplace_back(Clause{vector<Literal>{negLeft, *right}});
+		m_state.back().clauses.emplace_back(Clause{vector<Literal>{_left, negRight}});
+	}
+	else if (_right.name == "=" && parseLinearSum(_right.arguments.at(0)) && parseLinearSum(_right.arguments.at(1)))
+		// a = (x = y)  <=>  a = (x <= y && x >= y)
+		addBooleanEquality(
+			_left,
+			_right.arguments.at(0) <= _right.arguments.at(1) &&
+			_right.arguments.at(1) <= _right.arguments.at(0)
+		);
+	else
+	{
+		Literal a = parseLiteralOrReturnEqualBoolean(_right.arguments.at(0));
+		Literal b = parseLiteralOrReturnEqualBoolean(_right.arguments.at(1));
+		if (a.kind == Literal::Constraint && b.kind == Literal::Constraint)
+		{
+			// We cannot have more than one constraint per clause.
+			b = *parseLiteral(declareInternalBoolean());
+			addBooleanEquality(b, _right.arguments.at(1));
+		}
+
+		if (_right.name == "and")
+		{
+			// a = and(x, y) <=> (-a \/ x) /\ ( -a \/ y) /\ (a \/ -x \/ -y)
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{negate(_left), a}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{negate(_left), b}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a), negate(b)}});
+		}
+		else if (_right.name == "or")
+		{
+			// a = or(x, y) <=> (-a \/ x \/ y) /\ (a \/ -x) /\ (a \/ -y)
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{negate(_left), a, b}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a)}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{_left, negate(b)}});
+		}
+		else if (_right.name == "=")
+		{
+			// l = eq(a, b) <=> (-l or -a or b) and (-l or a or -b) and (l or -a or -b) and (l or a or b)
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{negate(_left), negate(a), b}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{negate(_left), a, negate(b)}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a), negate(b)}});
+			m_state.back().clauses.emplace_back(Clause{vector<Literal>{_left, a, b}});
+		}
+		else
+			solAssert(false, "Unsupported operation: " + _right.name);
+	}
+}
+
+
+// TODO as input we do not need the full solving state, only the bounds
+pair<CheckResult, map<string, rational>> BooleanLPSolver::runDPLL(SolvingState& _solvingState, DPLL _dpll)
+{
+	//cout << "Running dpll on" << endl << toString(_solvingState.bounds) << "\n" << toString(_dpll) << endl;
+
+	auto&& [simplifyResult, booleanModel] = _dpll.simplify();
+	if (!simplifyResult)
+		return {CheckResult::UNSATISFIABLE, {}};
+
+	//cout << "Simplified to" << endl << toString(_solvingState.bounds) << "\n" << toString(_dpll) << endl;
+
+	CheckResult result = CheckResult::UNKNOWN;
+	map<string, rational> model;
+	// TODO could run this check already even though not all variables are assigned
+	// and return unsat if it is already unsat.
+	if (_dpll.clauses.empty())
+	{
+		//cout << "Invoking LP..." << endl;
+		_solvingState.constraints.clear();
+		for (size_t c: _dpll.constraints)
+			_solvingState.constraints.emplace_back(constraint(c));
+		LPResult lpResult;
+		tie(lpResult, model) = m_lpSolver.check(_solvingState);
+		// LP solver is a rational solver, not an integer solver,
+		// so "feasible" does not mean there is an integer solution.
+
+		// TODO we could check the model to see if all variables are integer....s
+
+		// TODO if it is a pure boolean problem, we can actually answer "satisfiable"
+		switch (lpResult)
+		{
+		case LPResult::Infeasible:
+			result = CheckResult::UNSATISFIABLE;
+			break;
+		case LPResult::Unknown:
+		case LPResult::Unbounded:
+		case LPResult::Feasible:
+			result = CheckResult::UNKNOWN;
+		}
+	}
+	else
+	{
+		size_t varIndex = _dpll.findUnassignedVariable();
+
+		DPLL copy = _dpll;
+		if (_dpll.setVariable(varIndex, true))
+		{
+			booleanModel[varIndex] = true;
+			// cout << "Trying " << variableName(varIndex) << " = true\n";
+			tie(result, model) = runDPLL(_solvingState, move(_dpll));
+			// TODO actually we should also handle UNKNOWN here.
+		}
+		// TODO it will never be "satisfiable"
+		if (result != CheckResult::SATISFIABLE)
+		{
+			// cout << "Trying " << variableName(varIndex) << " = false\n";
+			if (!copy.setVariable(varIndex, false))
+				return {CheckResult::UNSATISFIABLE, {}};
+			booleanModel[varIndex] = false;
+			/*auto&& [result, model] = */runDPLL(_solvingState, move(copy));
+		}
+	}
+	if (result == CheckResult::SATISFIABLE)
+	{
+		for (auto const& [index, value]: booleanModel)
+			model[variableName(index)] = value ? 1 : 0;
+		return {result, move(model)};
+	}
+	else
+		return {result, {}};
+}
+
+string BooleanLPSolver::toString(DPLL const& _dpll) const
+{
+	string result;
+	for (size_t c: _dpll.constraints)
+		result += toString(Clause{{Literal{Literal::Constraint, c}}});
+	for (Clause const& c: _dpll.clauses)
+		result += toString(c);
+	return result;
+}
+
+string BooleanLPSolver::toString(std::vector<std::array<std::optional<boost::rational<bigint>>, 2>> const& _bounds) const
+{
+	string result;
+	for (auto&& [index, bounds]: _bounds | ranges::views::enumerate)
+	{
+		if (!bounds[0] && !bounds[1])
+			continue;
+		if (bounds[0])
+			result += ::toString(*bounds[0]) + " <= ";
+		// TODO If the variables are compressed, this does no longer work.
+		result += variableName(index);
+		if (bounds[1])
+			result += " <= " + ::toString(*bounds[1]);
+		result += "\n";
+	}
+	return result;
+}
+
+string BooleanLPSolver::toString(Clause const& _clause) const
+{
+	vector<string> literals;
+	for (Literal const& l: _clause.literals)
+		if (l.kind == Literal::Constraint)
+		{
+			Constraint const& constr = constraint(l.index);
+			vector<string> line;
+			for (auto&& [index, multiplier]: constr.data | ranges::views::enumerate)
+				if (index > 0 && multiplier != 0)
+				{
+					string mult =
+						multiplier == -1 ?
+						"-" :
+						multiplier == 1 ?
+						"" :
+						::toString(multiplier) + " ";
+					line.emplace_back(mult + variableName(index));
+				}
+			literals.emplace_back(joinHumanReadable(line, " + ") + (constr.equality ? "  = " : " <= ") + ::toString(constr.data.front()));
+		}
+		else
+			literals.emplace_back((l.kind == Literal::NegativeVariable ? "!" : "") + variableName(l.index));
+	return joinHumanReadable(literals, "  \\/  ") + "\n";
+}
+
+Constraint const& BooleanLPSolver::constraint(size_t _index) const
+{
+	for (State const& state: m_state)
+		if (state.constraints.count(_index))
+			return state.constraints.at(_index);
+	solAssert(false, "");
+}
+
+
+string BooleanLPSolver::variableName(size_t _index) const
+{
+	for (auto const& v: m_state.back().variables)
+		if (v.second == _index)
+			return v.first;
+	return {};
+}
+
+bool BooleanLPSolver::isBooleanVariable(string const& _name) const
+{
+	if (!m_state.back().variables.count(_name))
+		return false;
+	size_t index = m_state.back().variables.at(_name);
+	solAssert(index > 0, "");
+	return isBooleanVariable(index);
+}
+
+bool BooleanLPSolver::isBooleanVariable(size_t _index) const
+{
+	return
+		_index < m_state.back().isBooleanVariable.size() &&
+		m_state.back().isBooleanVariable.at(_index);
+}

libsolutil/BooleanLP.h

@@ -0,0 +1,148 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+#pragma once
+
+#include <libsmtutil/SolverInterface.h>
+
+#include <libsolutil/LP.h>
+
+#include <boost/rational.hpp>
+
+#include <vector>
+#include <variant>
+#include <stack>
+#include <compare>
+
+namespace solidity::util
+{
+
+/**
+ * A literal of a (potentially negated) boolean variable or an inactive constraint.
+ */
+struct Literal
+{
+	enum { PositiveVariable, NegativeVariable, Constraint } kind;
+	// Either points to a boolean variable or to a constraint.
+	size_t index{0};
+};
+
+/**
+ * A clause is a disjunction of literals.
+ */
+struct Clause
+{
+	std::vector<Literal> literals;
+};
+
+
+struct State
+{
+	bool infeasible = false;
+	std::map<std::string, size_t> variables;
+	std::vector<bool> isBooleanVariable;
+	// Potential constraints, referenced through clauses
+	std::map<size_t, Constraint> constraints;
+	// Unconditional bounds on variables
+	std::map<size_t, std::array<std::optional<boost::rational<bigint>>, 2>> bounds;
+
+	std::vector<Clause> clauses;
+};
+
+struct DPLL
+{
+	/// Try to simplify the set of clauses without branching.
+	/// @returns false if the set of clauses is unsatisfiable (without considering the constraints).
+	std::pair<bool, std::map<size_t, bool>> simplify();
+	size_t findUnassignedVariable() const;
+	bool setVariable(size_t _index, bool _value);
+	/// Sets variables and removes clauses or literals from clauses.
+	/// @returns false if the clauses are unsatisfiable.
+	bool setVariables(std::map<size_t, bool> const& _assignments, bool _removeSingleConstraintClauses = false);
+
+	std::vector<Clause> clauses;
+	std::vector<size_t> constraints;
+};
+
+
+class BooleanLPSolver: public smtutil::SolverInterface
+{
+public:
+	void reset() override;
+	void push() override;
+	void pop() override;
+
+	void declareVariable(std::string const& _name, smtutil::SortPointer const& _sort) override;
+
+	void addAssertion(smtutil::Expression const& _expr) override;
+
+	std::pair<smtutil::CheckResult, std::vector<std::string>>
+	check(std::vector<smtutil::Expression> const& _expressionsToEvaluate) override;
+
+	std::pair<smtutil::CheckResult, std::map<std::string, boost::rational<bigint>>> check();
+
+	std::string toString() const;
+
+private:
+	using rational = boost::rational<bigint>;
+
+	smtutil::Expression declareInternalBoolean();
+	void declareVariable(std::string const& _name, bool _boolean);
+
+	std::optional<Literal> parseLiteral(smtutil::Expression const& _expr);
+	Literal negate(Literal const& _lit);
+
+	Literal parseLiteralOrReturnEqualBoolean(smtutil::Expression const& _expr);
+
+	/// Parses the expression and expects a linear sum of variables.
+	/// Returns a vector with the first element being the constant and the
+	/// other elements the factors for the respective variables.
+	/// If the expression cannot be properly parsed or is not linear,
+	/// returns an empty vector.
+	std::optional<std::vector<rational>> parseLinearSum(smtutil::Expression const& _expression) const;
+	std::optional<std::vector<rational>> parseProduct(smtutil::Expression const& _expression) const;
+	std::optional<std::vector<rational>> parseFactor(smtutil::Expression const& _expression) const;
+
+	bool tryAddDirectBounds(Constraint const& _constraint);
+	void addUpperBound(size_t _index, rational _value);
+	void addLowerBound(size_t _index, rational _value);
+
+	size_t addConstraint(Constraint _constraint);
+
+	void addBooleanEquality(Literal const& _left, smtutil::Expression const& _right);
+
+	std::pair<smtutil::CheckResult, std::map<std::string, rational>> runDPLL(SolvingState& _solvingState, DPLL _dpll);
+	std::string toString(DPLL const& _dpll) const;
+	std::string toString(std::vector<std::array<std::optional<boost::rational<bigint>>, 2>> const& _bounds) const;
+	std::string toString(Clause const& _clause) const;
+
+	Constraint const& constraint(size_t _index) const;
+
+	std::string variableName(size_t _index) const;
+
+	bool isBooleanVariable(std::string const& _name) const;
+	bool isBooleanVariable(size_t _index) const;
+
+	size_t m_constraintCounter = 0;
+	size_t m_internalVariableCounter = 0;
+	/// Stack of state, to allow for push()/pop().
+	std::vector<State> m_state{{State{}}};
+	LPSolver m_lpSolver;
+};
+
+
+}

libsolutil/CMakeLists.txt

@@ -2,6 +2,8 @@ set(sources
 	Algorithms.h
 	AnsiColorized.h
 	Assertions.h
+	BooleanLP.cpp
+	BooleanLP.h
 	Common.h
 	CommonData.cpp
 	CommonData.h

test/CMakeLists.txt

@@ -31,6 +31,7 @@ set(contracts_sources
 detect_stray_source_files("${contracts_sources}" "contracts/")
 
 set(libsolutil_sources
+    libsolutil/BooleanLP.cpp
     libsolutil/Checksum.cpp
     libsolutil/CommonData.cpp
     libsolutil/CommonIO.cpp

test/libsolutil/BooleanLP.cpp

@@ -0,0 +1,322 @@
+/*
+	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/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolutil/BooleanLP.h>
+#include <libsolutil/RationalVectors.h>
+#include <libsmtutil/Sorts.h>
+#include <libsolutil/StringUtils.h>
+#include <test/Common.h>
+
+#include <boost/test/unit_test.hpp>
+
+using namespace std;
+using namespace solidity::smtutil;
+using namespace solidity::util;
+
+
+namespace solidity::util::test
+{
+
+
+class BooleanLPTestFramework
+{
+protected:
+	BooleanLPSolver solver;
+
+	Expression variable(string const& _name)
+	{
+		return solver.newVariable(_name, smtutil::SortProvider::sintSort);
+	}
+
+	Expression booleanVariable(string const& _name)
+	{
+		return solver.newVariable(_name, smtutil::SortProvider::boolSort);
+	}
+
+	void addAssertion(Expression const& _expr) { solver.addAssertion(_expr); }
+
+	void feasible(vector<pair<Expression, string>> const& _solution)
+	{
+		vector<Expression> variables;
+		vector<string> values;
+		for (auto const& [var, val]: _solution)
+		{
+			variables.emplace_back(var);
+			values.emplace_back(val);
+		}
+		auto [result, model] = solver.check(variables);
+		// TODO it actually never returns "satisfiable".
+		BOOST_CHECK(result == smtutil::CheckResult::SATISFIABLE);
+		BOOST_CHECK_EQUAL(joinHumanReadable(model), joinHumanReadable(values));
+	}
+
+	void infeasible()
+	{
+		auto [result, model] = solver.check({});
+		BOOST_CHECK(result == smtutil::CheckResult::UNSATISFIABLE);
+	}
+};
+
+
+
+BOOST_FIXTURE_TEST_SUITE(BooleanLP, BooleanLPTestFramework, *boost::unit_test::label("nooptions"))
+
+BOOST_AUTO_TEST_CASE(lower_bound)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	addAssertion(y >= 1);
+	addAssertion(x <= 10);
+	addAssertion(2 * x + y <= 2);
+	feasible({{x, "0"}, {y, "2"}});
+}
+
+BOOST_AUTO_TEST_CASE(check_infeasible)
+{
+	Expression x = variable("x");
+	addAssertion(x <= 3 && x >= 5);
+	infeasible();
+}
+
+BOOST_AUTO_TEST_CASE(unbounded)
+{
+	Expression x = variable("x");
+	addAssertion(x >= 2);
+	feasible({{x, "2"}});
+}
+
+BOOST_AUTO_TEST_CASE(unbounded_two)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	addAssertion(x + y >= 2);
+	addAssertion(x <= 10);
+	feasible({{x, "10"}, {y, "0"}});
+}
+
+BOOST_AUTO_TEST_CASE(equal)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	solver.addAssertion(x == y + 10);
+	solver.addAssertion(x <= 20);
+	feasible({{x, "20"}, {y, "10"}});
+}
+
+BOOST_AUTO_TEST_CASE(push_pop)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	solver.addAssertion(x + y <= 20);
+	feasible({{x, "20"}, {y, "0"}});
+
+	solver.push();
+	solver.addAssertion(x <= 5);
+	solver.addAssertion(y <= 5);
+	feasible({{x, "5"}, {y, "5"}});
+
+	solver.push();
+	solver.addAssertion(x >= 7);
+	infeasible();
+	solver.pop();
+
+	feasible({{x, "5"}, {y, "5"}});
+	solver.pop();
+
+	feasible({{x, "20"}, {y, "0"}});
+}
+
+BOOST_AUTO_TEST_CASE(less_than)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	solver.addAssertion(x == y + 1);
+	solver.push();
+	solver.addAssertion(y < x);
+	feasible({{x, "1"}, {y, "0"}});
+	solver.pop();
+	solver.push();
+	solver.addAssertion(y > x);
+	infeasible();
+	solver.pop();
+}
+
+BOOST_AUTO_TEST_CASE(equal_constant)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	solver.addAssertion(x < y);
+	solver.addAssertion(y == 5);
+	feasible({{x, "4"}, {y, "5"}});
+}
+
+BOOST_AUTO_TEST_CASE(chained_less_than)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	Expression z = variable("z");
+	solver.addAssertion(x < y && y < z);
+
+	solver.push();
+	solver.addAssertion(z == 0);
+	infeasible();
+	solver.pop();
+
+	solver.push();
+	solver.addAssertion(z == 1);
+	infeasible();
+	solver.pop();
+
+	solver.push();
+	solver.addAssertion(z == 2);
+	feasible({{x, "0"}, {y, "1"}, {z, "2"}});
+	solver.pop();
+}
+
+BOOST_AUTO_TEST_CASE(splittable)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	Expression z = variable("z");
+	Expression w = variable("w");
+	solver.addAssertion(x < y);
+	solver.addAssertion(x < y - 2);
+	solver.addAssertion(z + w == 28);
+
+	solver.push();
+	solver.addAssertion(z >= 30);
+	infeasible();
+	solver.pop();
+
+	solver.addAssertion(z >= 2);
+	feasible({{x, "0"}, {y, "3"}, {z, "2"}, {w, "26"}});
+	solver.push();
+	solver.addAssertion(z >= 4);
+	feasible({{x, "0"}, {y, "3"}, {z, "4"}, {w, "24"}});
+
+	solver.push();
+	solver.addAssertion(z < 4);
+	infeasible();
+	solver.pop();
+
+	// z >= 4 is still active
+	solver.addAssertion(z >= 3);
+	feasible({{x, "0"}, {y, "3"}, {z, "4"}, {w, "24"}});
+}
+
+
+BOOST_AUTO_TEST_CASE(boolean)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	Expression z = variable("z");
+	solver.addAssertion(x <= 5);
+	solver.addAssertion(y <= 2);
+	solver.push();
+	solver.addAssertion(x < y && x > y);
+	infeasible();
+	solver.pop();
+	Expression w = booleanVariable("w");
+	solver.addAssertion(w == (x < y));
+	solver.addAssertion(w || x > y);
+	feasible({{x, "0"}, {y, "3"}, {z, "2"}, {w, "26"}});
+}
+
+BOOST_AUTO_TEST_CASE(boolean_complex)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	Expression a = booleanVariable("a");
+	Expression b = booleanVariable("b");
+	solver.addAssertion(x <= 5);
+	solver.addAssertion(y <= 2);
+	solver.addAssertion(a == (x >= 2));
+	solver.addAssertion(a || b);
+	solver.addAssertion(b == !a);
+	solver.addAssertion(b == (x < 2));
+	feasible({{a, "1"}, {b, "0"}, {x, "5"}, {y, "2"}});
+	solver.addAssertion(a && b);
+	infeasible();
+}
+
+BOOST_AUTO_TEST_CASE(magic_square)
+{
+	vector<Expression> vars;
+	for (size_t i = 0; i < 9; i++)
+		vars.push_back(variable(string{static_cast<char>('a' + i)}));
+	for (Expression const& var: vars)
+		solver.addAssertion(1 <= var && var <= 9);
+	// If we assert all to be mutually distinct, the problems gets too large.
+	for (size_t i = 0; i < 9; i++)
+		for (size_t j = i + 7; j < 9; j++)
+			solver.addAssertion(vars[i] != vars[j]);
+	for (size_t i = 0; i < 4; i++)
+		solver.addAssertion(vars[i] != vars[i + 1]);
+	for (size_t i = 0; i < 3; i++)
+		solver.addAssertion(vars[i] + vars[i + 3] + vars[i + 6] == 15);
+	for (size_t i = 0; i < 9; i += 3)
+		solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] == 15);
+	feasible({
+		{vars[0], "1"}, {vars[1], "0"}, {vars[2], "5"},
+		{vars[3], "1"}, {vars[4], "0"}, {vars[5], "5"},
+		{vars[6], "1"}, {vars[7], "0"}, {vars[8], "5"}
+	});
+}
+
+BOOST_AUTO_TEST_CASE(boolean_complex_2)
+{
+	Expression x = variable("x");
+	Expression y = variable("y");
+	Expression a = booleanVariable("a");
+	Expression b = booleanVariable("b");
+	solver.addAssertion(x != 20);
+	feasible({{x, "19"}});
+	solver.addAssertion(x <= 5 || (x > 7 && x != 8));
+	solver.addAssertion(a = (x == 9));
+	feasible({{a, "1"}, {b, "0"}, {x, "5"}});
+//	solver.addAssertion(!a || (x == 10));
+//	solver.addAssertion(b == !a);
+//	solver.addAssertion(b == (x < 200));
+//	feasible({{a, "1"}, {b, "0"}, {x, "5"}});
+//	solver.addAssertion(a && b);
+//	infeasible();
+}
+
+
+BOOST_AUTO_TEST_CASE(pure_boolean)
+{
+	Expression a = booleanVariable("a");
+	Expression b = booleanVariable("b");
+	Expression c = booleanVariable("c");
+	Expression d = booleanVariable("d");
+	Expression e = booleanVariable("e");
+	Expression f = booleanVariable("f");
+	solver.addAssertion(a && !b);
+	solver.addAssertion(b || c);
+	solver.addAssertion(c == (d || c));
+	solver.addAssertion(f == (b && !c));
+	solver.addAssertion(!f || e);
+	solver.addAssertion(c || d);
+	feasible({});
+	solver.addAssertion(a && b);
+	infeasible();
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+}