diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp new file mode 100644 index 000000000..ba1541fa9 --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include +#include +#include + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +using namespace std; +using namespace solidity; +using namespace solidity::util; +using namespace solidity::smtutil; + +using rational = boost::rational; + + +pair> DPLL::simplify() +{ + // TODO use vector? + map 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 const& _assignments, bool _removeSingleConstraintClauses) +{ + // TODO do this in a way so that we do not have to copy twice. + vector prunedClauses; + for (Clause const& c: clauses) + { + bool skipClause = false; + vector 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{}}}; + 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 variables = m_state.back().variables; + map>, 2>> bounds = m_state.back().bounds; + vector 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 '$' + 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{*parseLiteral(_expr)}}); + else if (_expr.name == "=") + { + // Try to see if both sides are linear. + optional> left = parseLinearSum(_expr.arguments.at(0)); + optional> right = parseLinearSum(_expr.arguments.at(1)); + if (left && right) + { + vector 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::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{left, right}}); + } + else if (_expr.name == "not") + { + Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0))); + m_state.back().clauses.emplace_back(Clause{vector{l}}); + } + else if (_expr.name == "<=") + { + optional> left = parseLinearSum(_expr.arguments.at(0)); + optional> right = parseLinearSum(_expr.arguments.at(1)); + if (!left || !right) + return; + + vector 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::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> BooleanLPSolver::check(vector const& _expressionsToEvaluate) +{ + cout << "Solving boolean constraint system" << endl; + cout << toString() << endl; + + if (m_state.back().infeasible) + return make_pair(CheckResult::UNSATISFIABLE, vector{}); + + // 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 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 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 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> left = parseLinearSum(_expr.arguments.at(0)); + optional> right = parseLinearSum(_expr.arguments.at(1)); + if (!left || !right) + return {}; + + vector 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 = parseLiteral(_expr)) + return *literal; + else + { + Literal newBoolean = *parseLiteral(declareInternalBoolean()); + addBooleanEquality(newBoolean, _expr); + return newBoolean; + } +} + +optional> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr) const +{ + if (_expr.arguments.empty() || _expr.name == "*") + return parseProduct(_expr); + else if (_expr.name == "+" || _expr.name == "-") + { + optional> left = parseLinearSum(_expr.arguments.at(0)); + optional> 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> 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> 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(bigint(_expr.name))}; + else if (_expr.name == "true") + return vector{rational(bigint(1))}; + else if (_expr.name == "false") + return vector{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 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 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{negLeft, *right}}); + m_state.back().clauses.emplace_back(Clause{vector{_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{negate(_left), a}}); + m_state.back().clauses.emplace_back(Clause{vector{negate(_left), b}}); + m_state.back().clauses.emplace_back(Clause{vector{_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{negate(_left), a, b}}); + m_state.back().clauses.emplace_back(Clause{vector{_left, negate(a)}}); + m_state.back().clauses.emplace_back(Clause{vector{_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{negate(_left), negate(a), b}}); + m_state.back().clauses.emplace_back(Clause{vector{negate(_left), a, negate(b)}}); + m_state.back().clauses.emplace_back(Clause{vector{_left, negate(a), negate(b)}}); + m_state.back().clauses.emplace_back(Clause{vector{_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> 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 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>, 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 literals; + for (Literal const& l: _clause.literals) + if (l.kind == Literal::Constraint) + { + Constraint const& constr = constraint(l.index); + vector 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); +} diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h new file mode 100644 index 000000000..04c6a5153 --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 +#pragma once + +#include + +#include + +#include + +#include +#include +#include +#include + +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 literals; +}; + + +struct State +{ + bool infeasible = false; + std::map variables; + std::vector isBooleanVariable; + // Potential constraints, referenced through clauses + std::map constraints; + // Unconditional bounds on variables + std::map>, 2>> bounds; + + std::vector 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> 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 const& _assignments, bool _removeSingleConstraintClauses = false); + + std::vector clauses; + std::vector 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> + check(std::vector const& _expressionsToEvaluate) override; + + std::pair>> check(); + + std::string toString() const; + +private: + using rational = boost::rational; + + smtutil::Expression declareInternalBoolean(); + void declareVariable(std::string const& _name, bool _boolean); + + std::optional 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> parseLinearSum(smtutil::Expression const& _expression) const; + std::optional> parseProduct(smtutil::Expression const& _expression) const; + std::optional> 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> runDPLL(SolvingState& _solvingState, DPLL _dpll); + std::string toString(DPLL const& _dpll) const; + std::string toString(std::vector>, 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 m_state{{State{}}}; + LPSolver m_lpSolver; +}; + + +} diff --git a/libsolutil/CMakeLists.txt b/libsolutil/CMakeLists.txt index a1d915bb3..be2900223 100644 --- a/libsolutil/CMakeLists.txt +++ b/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 diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 73a3fef4f..d1f333fab 100644 --- a/test/CMakeLists.txt +++ b/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 diff --git a/test/libsolutil/BooleanLP.cpp b/test/libsolutil/BooleanLP.cpp new file mode 100644 index 000000000..a1de4ec07 --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include +#include +#include +#include +#include + +#include + +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> const& _solution) + { + vector variables; + vector 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 vars; + for (size_t i = 0; i < 9; i++) + vars.push_back(variable(string{static_cast('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() + +}