diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp new file mode 100644 index 000000000..42320f99f --- /dev/null +++ b/libsolutil/BooleanLP.cpp @@ -0,0 +1,610 @@ +/* + 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 +#include + +#include + +using namespace std; +using namespace solidity; +using namespace solidity::util; +using namespace solidity::smtutil; + +using rational = boost::rational; + +namespace +{ +template +void resizeAndSet(vector& _vector, size_t _index, T _value) +{ + if (_vector.size() < _index + 1) + _vector.resize(_index + 1); + _vector[_index] = move(_value); +} + +string toString(rational const& _x) +{ + if (_x.denominator() == 1) + return _x.numerator().str(); + else + return _x.numerator().str() + "/" + _x.denominator().str(); +} + +} + +void BooleanLPSolver::reset() +{ + m_state = vector{{State{}}}; + // TODO retain an instance of the LP solver, it should keep its cache! +} + +void BooleanLPSolver::push() +{ + // TODO maybe find a way where we do not have to copy everything + State currentState = state(); + m_state.emplace_back(move(currentState)); +} + +void BooleanLPSolver::pop() +{ + m_state.pop_back(); + solAssert(!m_state.empty(), ""); +} + +void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _sort) +{ + // Internal variables are '$', or '$c' so escape `$` to `$$`. + 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(!state().variables.count(name), ""); + declareVariable(name, _sort->kind == Kind::Bool); +} + +void BooleanLPSolver::addAssertion(Expression const& _expr) +{ + if (_expr.arguments.empty()) + state().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) + { + LinearExpression data = *left - *right; + data[0] *= -1; + Constraint c{move(data), _expr.name == "=", {}}; + if (!tryAddDirectBounds(c)) + state().fixedConstraints.emplace_back(move(c)); + } + 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 (isConditionalConstraint(left.variable) && isConditionalConstraint(right.variable)) + { + // We cannot have more than one constraint per clause. + // TODO Why? + right = *parseLiteral(declareInternalBoolean()); + addBooleanEquality(right, _expr.arguments.at(1)); + } + state().clauses.emplace_back(Clause{vector{left, right}}); + } + else if (_expr.name == "not") + { + // TODO can we still try to add a fixed constraint? + Literal l = negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0))); + state().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) + { + cout << "Unable to parse expression" << endl; + // TODO fail in some way + return; + } + + LinearExpression data = *left - *right; + data[0] *= -1; + Constraint c{move(data), _expr.name == "=", {}}; + if (!tryAddDirectBounds(c)) + state().fixedConstraints.emplace_back(move(c)); + } + 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)); + else + cout << "Unknown operator " << _expr.name << endl; +} + + +pair> BooleanLPSolver::check(vector const&) +{ + cout << "Solving boolean constraint system" << endl; + cout << toString() << endl; + cout << "--------------" << endl; + + if (state().infeasible) + return make_pair(CheckResult::UNSATISFIABLE, vector{}); + + std::vector booleanVariables; + std::vector clauses = state().clauses; + SolvingState lpState; + for (auto&& [index, bound]: state().bounds) + resizeAndSet(lpState.bounds, index, bound); + lpState.constraints = state().fixedConstraints; + // TODO this way, it will result in a lot of gaps in both sets of variables. + // should we compress them and store a mapping? + // Is it even a problem if the indices overlap? + for (auto&& [name, index]: state().variables) + if (state().isBooleanVariable.at(index)) + resizeAndSet(booleanVariables, index, name); + else + resizeAndSet(lpState.variableNames, index, name); + + cout << "Running LP solver on fixed constraints." << endl; + if (m_lpSolver.check(lpState).first == LPResult::Infeasible) + return {CheckResult::UNSATISFIABLE, {}}; + + auto theorySolver = [&](map const& _booleanAssignment) -> optional + { + SolvingState lpStateToCheck = lpState; + for (auto&& [constraintIndex, value]: _booleanAssignment) + { + if (!state().conditionalConstraints.count(constraintIndex)) + continue; + // assert that value is true? + // "reason" is already stored for those constraints. + Constraint const& constraint = state().conditionalConstraints.at(constraintIndex); + solAssert( + constraint.reasons.size() == 1 && + *constraint.reasons.begin() == constraintIndex + ); + lpStateToCheck.constraints.emplace_back(constraint); + } + auto&& [result, modelOrReason] = m_lpSolver.check(move(lpStateToCheck)); + // We can only really use the result "infeasible". Everything else should be "sat". + if (result == LPResult::Infeasible) + { + // TODO this could be the empty clause if the LP is already infeasible + // with only the fixed constraints - run it beforehand! + // TODO is it ok to ignore the non-constraint boolean variables here? + Clause conflictClause; + for (size_t constraintIndex: get(modelOrReason)) + conflictClause.emplace_back(Literal{false, constraintIndex}); + return conflictClause; + } + else + return nullopt; + }; + + auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver}.solve(); + if (!optionalModel) + return {CheckResult::UNSATISFIABLE, {}}; + else + return {CheckResult::UNKNOWN, {}}; +} + +string BooleanLPSolver::toString() const +{ + string result; + + result += "-- Fixed Constraints:\n"; + for (Constraint const& c: state().fixedConstraints) + result += toString(c) + "\n"; + result += "-- Fixed Bounds:\n"; + for (auto&& [index, bounds]: state().bounds) + { + if (!bounds.lower && !bounds.upper) + continue; + if (bounds.lower) + result += ::toString(*bounds.lower) + " <= "; + result += variableName(index); + if (bounds.upper) + result += " <= " + ::toString(*bounds.upper); + result += "\n"; + } + result += "-- Clauses:\n"; + for (Clause const& c: state().clauses) + result += toString(c); + return result; +} + +Expression BooleanLPSolver::declareInternalBoolean() +{ + string name = "$" + to_string(state().variables.size() + 1); + declareVariable(name, true); + return smtutil::Expression(name, {}, SortProvider::boolSort); +} + +void BooleanLPSolver::declareVariable(string const& _name, bool _boolean) +{ + size_t index = state().variables.size() + 1; + state().variables[_name] = index; + resizeAndSet(state().isBooleanVariable, index, _boolean); +} + +optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr) +{ + // TODO constanst true/false? + + if (_expr.arguments.empty()) + { + if (isBooleanVariable(_expr.name)) + return Literal{ + true, + state().variables.at(_expr.name) + }; + else + cout << "cannot encode " << _expr.name << " - not a boolean literal variable." << endl; + } + 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 {}; + + LinearExpression data = *left - *right; + data[0] *= -1; + + return Literal{true, addConditionalConstraint(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) +{ + if (isConditionalConstraint(_lit.variable)) + { + Constraint const& c = conditionalConstraint(_lit.variable); + solAssert(!c.equality, ""); + + // X > b + // -x < -b + // -x <= -b - 1 + + Constraint negated = c; + negated.data *= -1; + negated.data[0] -= 1; + return Literal{true, addConditionalConstraint(negated)}; + } + else + return ~_lit; +} + +Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr) +{ + // TODO hen can this fail? + 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 == "+" ? *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 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 LinearExpression::constant(rational(bigint(_expr.name))); + else if (_expr.name == "true") + // TODO do we want to do this? + return LinearExpression::constant(1); + else if (_expr.name == "false") + // TODO do we want to do this? + return LinearExpression::constant(0); + + size_t index = state().variables.at(_expr.name); + solAssert(index > 0, ""); + if (isBooleanVariable(index)) + return nullopt; + return LinearExpression::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; + state().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 (!state().bounds[_index].upper || _value < *state().bounds[_index].upper) + state().bounds[_index].upper = 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 (!state().bounds[_index].lower || _value > *state().bounds[_index].lower) + state().bounds[_index].lower = move(_value); +} + +size_t BooleanLPSolver::addConditionalConstraint(Constraint _constraint) +{ + string name = "$c" + to_string(state().variables.size() + 1); + // It's not a boolean variable + // TODO we actually have there kinds of variables and we should split them: + // - actual booleans (including internals) + // - conditional constraints + // - integers + declareVariable(name, false); + size_t index = state().variables.at(name); + solAssert(_constraint.reasons.empty()); + _constraint.reasons.emplace(index); + state().conditionalConstraints[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); + state().clauses.emplace_back(Clause{vector{negLeft, *right}}); + state().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 (isConditionalConstraint(a.variable) && isConditionalConstraint(b.variable)) + { + // We cannot have more than one constraint per clause. + // TODO Why? + b = *parseLiteral(declareInternalBoolean()); + addBooleanEquality(b, _right.arguments.at(1)); + } + + if (_right.name == "and") + { + // a = and(x, y) <=> (-a \/ x) /\ ( -a \/ y) /\ (a \/ -x \/ -y) + state().clauses.emplace_back(Clause{vector{negate(_left), a}}); + state().clauses.emplace_back(Clause{vector{negate(_left), b}}); + state().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) + state().clauses.emplace_back(Clause{vector{negate(_left), a, b}}); + state().clauses.emplace_back(Clause{vector{_left, negate(a)}}); + state().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) + state().clauses.emplace_back(Clause{vector{negate(_left), negate(a), b}}); + state().clauses.emplace_back(Clause{vector{negate(_left), a, negate(b)}}); + state().clauses.emplace_back(Clause{vector{_left, negate(a), negate(b)}}); + state().clauses.emplace_back(Clause{vector{_left, a, b}}); + } + else + solAssert(false, "Unsupported operation: " + _right.name); + } +} + +/* +string BooleanLPSolver::toString(std::vector const& _bounds) const +{ + string result; + for (auto&& [index, bounds]: _bounds | ranges::views::enumerate) + { + if (!bounds.lower && !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) + if (isBooleanVariable(l.variable)) + literals.emplace_back((l.positive ? "" : "!") + variableName(l.variable)); + else + { + solAssert(isConditionalConstraint(l.variable)); + solAssert(l.positive); + literals.emplace_back(toString(conditionalConstraint(l.variable))); + } + return joinHumanReadable(literals, " \\/ ") + "\n"; +} + +string BooleanLPSolver::toString(Constraint const& _constraint) const +{ + vector line; + for (auto&& [index, multiplier]: _constraint.data | ranges::views::enumerate) + if (index > 0 && multiplier != 0) + { + string mult = + multiplier == -1 ? + "-" : + multiplier == 1 ? + "" : + ::toString(multiplier) + " "; + line.emplace_back(mult + variableName(index)); + } + // TODO reasons? + return + joinHumanReadable(line, " + ") + + (_constraint.equality ? " = " : " <= ") + + ::toString(_constraint.data.front()); +} + +Constraint const& BooleanLPSolver::conditionalConstraint(size_t _index) const +{ + return state().conditionalConstraints.at(_index); +} + +string BooleanLPSolver::variableName(size_t _index) const +{ + for (auto const& v: state().variables) + if (v.second == _index) + return v.first; + return {}; +} + +bool BooleanLPSolver::isBooleanVariable(string const& _name) const +{ + if (!state().variables.count(_name)) + return false; + size_t index = state().variables.at(_name); + solAssert(index > 0, ""); + return isBooleanVariable(index); +} + +bool BooleanLPSolver::isBooleanVariable(size_t _index) const +{ + return + _index < state().isBooleanVariable.size() && + state().isBooleanVariable.at(_index); +} diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h new file mode 100644 index 000000000..8e6a2911b --- /dev/null +++ b/libsolutil/BooleanLP.h @@ -0,0 +1,130 @@ +/* + 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 +#include + +namespace solidity::util +{ + +struct State +{ + bool infeasible = false; + std::map variables; + std::vector isBooleanVariable; + // Potential constraints, referenced through clauses + std::map conditionalConstraints; + std::vector clauses; + + // Unconditional bounds on variables + std::map bounds; + // Unconditional constraints + std::vector fixedConstraints; +}; + +/** + * Component that satisfies the SMT SolverInterface and uses an LP solver plus the DPLL + * algorithm internally. + * It uses a rational relaxation of the integer program and thus will not be able to answer + * "satisfiable", but its answers are still correct. + * + * TODO are integers always non-negative? + * + * Integers are unbounded. + */ +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 addConditionalConstraint(Constraint _constraint); + + void addBooleanEquality(Literal const& _left, smtutil::Expression const& _right); + + //std::string toString(std::vector const& _bounds) const; + std::string toString(Clause const& _clause) const; + std::string toString(Constraint const& _constraint) const; + + Constraint const& conditionalConstraint(size_t _index) const; + + std::string variableName(size_t _index) const; + + bool isBooleanVariable(std::string const& _name) const; + bool isBooleanVariable(size_t _index) const; + bool isConditionalConstraint(size_t _index) const { return state().conditionalConstraints.count(_index); } + + State& state() { return m_state.back(); } + State const& state() const { return m_state.back(); } + + /// Stack of state, to allow for push()/pop(). + std::vector m_state{{State{}}}; + // TODO this is only here so that it can keep its cache. + // It might be better to just have the cache here. + // Although its stote is only the cache in the end... + LPSolver m_lpSolver{false}; +}; + + +} diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h index 0bbf2cde9..bc0118c58 100644 --- a/libsolutil/CDCL.h +++ b/libsolutil/CDCL.h @@ -33,9 +33,10 @@ namespace solidity::util */ struct Literal { + // TODO do we need to init them? bool positive; // Either points to a boolean variable or to a constraint. - size_t variable{0}; + size_t variable; Literal operator~() const { return Literal{!positive, variable}; } bool operator==(Literal const& _other) const diff --git a/libsolutil/CMakeLists.txt b/libsolutil/CMakeLists.txt index 9a9d97c8c..077d9f1e6 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 CDCL.h CDCL.cpp Common.h diff --git a/libsolutil/LP.h b/libsolutil/LP.h index cc222df2c..a586ef0e3 100644 --- a/libsolutil/LP.h +++ b/libsolutil/LP.h @@ -63,6 +63,8 @@ struct SolvingState bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); } bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); } + // TOOD this is currently not used + /// Set of literals the conjunction of which implies the lower bonud. std::set lowerReasons; /// Set of literals the conjunction of which implies the upper bonud. diff --git a/libsolutil/LinearExpression.h b/libsolutil/LinearExpression.h index 66b3a827d..bdfdae642 100644 --- a/libsolutil/LinearExpression.h +++ b/libsolutil/LinearExpression.h @@ -55,6 +55,14 @@ public: return result; } + static LinearExpression constant(rational _factor) + { + LinearExpression result; + result.resize(1); + result[0] = std::move(_factor); + return result; + } + rational const& get(size_t _index) const { static rational const zero; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index a35cfb772..f6a58acd8 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/CDCL.cpp libsolutil/Checksum.cpp libsolutil/CommonData.cpp diff --git a/test/libsolutil/BooleanLP.cpp b/test/libsolutil/BooleanLP.cpp new file mode 100644 index 000000000..7f810347b --- /dev/null +++ b/test/libsolutil/BooleanLP.cpp @@ -0,0 +1,348 @@ +/* + 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_3) +{ + vector vars; + for (size_t i = 0; i < 9; i++) + vars.push_back(variable(string{static_cast('a' + i)})); + Expression sum = variable("sum"); + for (Expression const& var: vars) + solver.addAssertion(1 <= var && var <= 9); + for (size_t i = 0; i < 9; i++) + for (size_t j = i + 1; j < 9; j++) + solver.addAssertion(vars[i] != vars[j]); + for (size_t i = 0; i < 3; i++) + solver.addAssertion(vars[i] + vars[i + 3] + vars[i + 6] == sum); + for (size_t i = 0; i < 9; i += 3) + solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] == sum); + solver.addAssertion(vars[0] + vars[4] + vars[8] == sum); + solver.addAssertion(vars[2] + vars[4] + vars[6] == sum); + feasible({ + {sum, "15"}, + {vars[0], "8"}, {vars[1], "3"}, {vars[2], "4"}, + {vars[3], "1"}, {vars[4], "5"}, {vars[5], "9"}, + {vars[6], "6"}, {vars[7], "7"}, {vars[8], "2"} + }); +} + +// This still takes too long. +// +//BOOST_AUTO_TEST_CASE(magic_square_4) +//{ +// vector vars; +// for (size_t i = 0; i < 16; i++) +// vars.push_back(variable(string{static_cast('a' + i)})); +// for (Expression const& var: vars) +// solver.addAssertion(1 <= var && var <= 16); +// for (size_t i = 0; i < 16; i++) +// for (size_t j = i + 1; j < 16; j++) +// solver.addAssertion(vars[i] != vars[j]); +// for (size_t i = 0; i < 4; i++) +// solver.addAssertion(vars[i] + vars[i + 4] + vars[i + 8] + vars[i + 12] == 34); +// for (size_t i = 0; i < 16; i += 4) +// solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] + vars[i + 3] == 34); +// solver.addAssertion(vars[0] + vars[5] + vars[10] + vars[15] == 34); +// solver.addAssertion(vars[3] + vars[6] + vars[9] + vars[12] == 34); +// feasible({ +// {vars[0], "9"}, {vars[1], "5"}, {vars[2], "1"}, +// {vars[3], "4"}, {vars[4], "3"}, {vars[5], "8"}, +// {vars[6], "2"}, {vars[7], "7"}, {vars[8], "6"} +// }); +//} + +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, "21"}}); + solver.addAssertion(x <= 5 || (x > 7 && x != 8)); + solver.addAssertion(a == (x == 9)); + feasible({{a, "0"}, {b, "unknown"}, {x, "21"}}); + solver.addAssertion(!a || (x == 10)); + solver.addAssertion(b == !a); + solver.addAssertion(b == (x < 200)); + feasible({{a, "0"}, {b, "1"}, {x, "199"}}); + 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() + +}