diff --git a/.gitmodules b/.gitmodules index 6ad08ddfd..c28bb72c3 100644 --- a/.gitmodules +++ b/.gitmodules @@ -20,3 +20,6 @@ [submodule "third_party/variant"] path = third_party/variant url = ../../mpark/variant.git +[submodule "third_party/wide-integer"] + path = third_party/wide-integer + url = ../../ckormanyos/wide-integer.git diff --git a/libgringo/CMakeLists.txt b/libgringo/CMakeLists.txt index f28169152..bbada06c5 100644 --- a/libgringo/CMakeLists.txt +++ b/libgringo/CMakeLists.txt @@ -126,7 +126,7 @@ set(source # ]]] add_library(libgringo STATIC ${header} ${source}) -target_link_libraries(libgringo PUBLIC libpotassco libreify tsl::ordered_map tsl::hopscotch_map tsl::sparse_map tl::optional mpark::variant) +target_link_libraries(libgringo PUBLIC libpotassco libreify tsl::ordered_map tsl::hopscotch_map tsl::sparse_map tl::optional mpark::variant math::wide_integer) target_include_directories(libgringo PUBLIC "$" diff --git a/libgringo/gringo/term.hh b/libgringo/gringo/term.hh index 1bdc23992..daa48c182 100644 --- a/libgringo/gringo/term.hh +++ b/libgringo/gringo/term.hh @@ -193,7 +193,7 @@ private: }; struct IETerm { - int coefficient{0}; + int64_t coefficient{0}; VarTerm const *variable{nullptr}; }; using IETermVec = std::vector; @@ -203,7 +203,7 @@ void subIETerm(IETermVec &terms, IETerm const &term); struct IE { IETermVec terms; - int bound; + int64_t bound; }; using IEVec = std::vector; @@ -259,10 +259,7 @@ public: void compute(); private: - enum class UpdateResult { changed, unchanged, overflow }; using SubSolvers = std::forward_list; - UpdateResult update_bound_(IETerm const &term, int64_t slack, int num_unbounded); - bool update_slack_(IETerm const &term, int64_t &slack, int &num_unbounded); IESolver *parent_; IEContext &ctx_; diff --git a/libgringo/src/term.cc b/libgringo/src/term.cc index 480c185b8..91d7d2e40 100644 --- a/libgringo/src/term.cc +++ b/libgringo/src/term.cc @@ -22,17 +22,22 @@ // }}} +#include +#include + +#include + #include "gringo/term.hh" #include "gringo/base.hh" #include "gringo/logger.hh" #include "gringo/graph.hh" -#include -#include // #define CLINGO_DEBUG_INEQUALITIES namespace Gringo { +using slack_t = math::wide_integer::int128_t; + // {{{ definition of Defines Defines::DefMap const &Defines::defs() const { @@ -156,6 +161,130 @@ void Defines::apply(Symbol x, Symbol &retVal, UTerm &retTerm, bool replace) { // {{{ definition of IESolver +namespace { + +slack_t floordiv(slack_t n, slack_t m) { + auto a = n / m; + auto b = n % m; + if (((n < 0) != (m < 0)) && b != 0) { + --a; + } + return a; +} + +slack_t ceildiv(slack_t n, slack_t m) { + auto a = n / m; + auto b = n % m; + if (((n < 0) != (m < 0)) && b != 0) { + ++a; + } + return a; +} + +template +I div(bool positive, I a, I b) { + return positive ? floordiv(a, b) : ceildiv(a, b); +} + +template +int clamp(I a) { + if (a > std::numeric_limits::max()) { + return std::numeric_limits::max(); + } + if (a < std::numeric_limits::min()) { + return std::numeric_limits::min(); + } + return static_cast(a); + +} + +int clamp_div(bool positive, slack_t a, int64_t b) { + if (a == std::numeric_limits::min() && b == -1) { + return std::numeric_limits::max(); + } + return clamp(div(positive, a, b)); +} + +template +It merge_adjancent(It first, It last, Merge m) { + if (first == last) { + return last; + } + + auto result = first; + while (++first != last) { + if (!m(*result, *first) && ++result != first) { + *result = std::move(*first); + } + } + return ++result; +} + +bool update_bound(IEBoundMap &bounds, IETerm const &term, slack_t slack, int num_unbounded) { + bool positive = term.coefficient > 0; + auto type = positive ? IEBound::Upper : IEBound::Lower; + if (num_unbounded == 0) { + slack += static_cast(term.coefficient) * bounds[term.variable].get(type); + } + else if (num_unbounded > 1 || bounds[term.variable].isSet(type)) { + return false; + } + + auto value = clamp_div(positive, slack, term.coefficient); + return bounds[term.variable].refine(positive ? IEBound::Lower : IEBound::Upper, value); +} + +void update_slack(IEBoundMap &bounds, IETerm const &term, slack_t &slack, int &num_unbounded) { + auto type = term.coefficient > 0 ? IEBound::Upper : IEBound::Lower; + if (bounds[term.variable].isSet(type)) { + slack -= static_cast(term.coefficient) * bounds[term.variable].get(type); + } + else { + ++num_unbounded; + } +} + +#ifdef CLINGO_DEBUG_INEQUALITIES + +std::ostream &operator<<(std::ostream &out, IEBound const &bound) { + out << "["; + if (bound.isSet(IEBound::Lower)) { + out << bound.get(IEBound::Lower); + } + else { + out << "-inf"; + } + out << ","; + if (bound.isSet(IEBound::Upper)) { + out << bound.get(IEBound::Upper); + } + else { + out << "+inf"; + } + out << "]"; + return out; +} + +std::ostream &operator<<(std::ostream &out, IE const &ie) { + bool comma = false; + if (ie.terms.empty()) { + out << "0"; + } + for (auto const &term : ie.terms) { + if (comma) { + out << " + "; + } + comma = true; + out << term.coefficient << "*" << term.variable->name; + } + out << " >= " << ie.bound; + return out; +} + +#endif + +} // namespace + bool IEBound::isSet(Type type) const { return type == Lower ? hasLower_ : hasUpper_; } @@ -225,25 +354,6 @@ bool IESolver::isImproving(VarTerm const *var, IEBound const &bound) const { return bound.isImproving(it->second); } -namespace { - -template -It merge_adjancent(It first, It last, Merge m) { - if (first == last) { - return last; - } - - auto result = first; - while (++first != last) { - if (!m(*result, *first) && ++result != first) { - *result = std::move(*first); - } - } - return ++result; -} - -} // namespace - void IESolver::add(IE ie, bool ignoreIfFixed) { auto &terms = ie.terms; @@ -280,57 +390,14 @@ void IESolver::add(IE ie, bool ignoreIfFixed) { if (ies_.back().terms.size() == 1 && ignoreIfFixed) { auto term = ies_.back().terms.back(); if (term.coefficient == 1) { - fixed_[term.variable].refine(IEBound::Lower, ies_.back().bound); + fixed_[term.variable].refine(IEBound::Lower, clamp(ies_.back().bound)); } else if (term.coefficient == -1) { - fixed_[term.variable].refine(IEBound::Upper, -ies_.back().bound); + fixed_[term.variable].refine(IEBound::Upper, clamp(-ies_.back().bound)); } } } -#ifdef CLINGO_DEBUG_INEQUALITIES - -namespace { - -std::ostream &operator<<(std::ostream &out, IEBound const &bound) { - out << "["; - if (bound.isSet(IEBound::Lower)) { - out << bound.get(IEBound::Lower); - } - else { - out << "-inf"; - } - out << ","; - if (bound.isSet(IEBound::Upper)) { - out << bound.get(IEBound::Upper); - } - else { - out << "+inf"; - } - out << "]"; - return out; -} - -std::ostream &operator<<(std::ostream &out, IE const &ie) { - bool comma = false; - if (ie.terms.empty()) { - out << "0"; - } - for (auto const &term : ie.terms) { - if (comma) { - out << " + "; - } - comma = true; - out << term.coefficient << "*" << term.variable->name; - } - out << " >= " << ie.bound; - return out; -} - -} // namespace - -#endif - void IESolver::compute() { #ifdef CLINGO_DEBUG_INEQUALITIES for (auto &ie : ies_) { @@ -352,16 +419,11 @@ void IESolver::compute() { while (changed) { changed = false; for (auto const &ie : ies_) { - int64_t slack = ie.bound; + slack_t slack = ie.bound; int num_unbounded = 0; for (auto const &term : ie.terms) { // In case the slack cannot be updated due to an overflow, no bounds are calculated. - if (!update_slack_(term, slack, num_unbounded)) { -#ifdef CLINGO_DEBUG_INEQUALITIES - std::cerr << " overflow updating slack of " << ie << std::endl; -#endif - return; - } + update_slack(bounds_, term, slack, num_unbounded); } if (num_unbounded == 0 && slack > 0) { // we simply set all bounds to empty intervals @@ -376,20 +438,13 @@ void IESolver::compute() { } if (num_unbounded <= 1) { for (auto const &term : ie.terms) { - auto res = update_bound_(term, slack, num_unbounded); - if (res == UpdateResult::changed) { + if (update_bound(bounds_, term, slack, num_unbounded)) { #ifdef CLINGO_DEBUG_INEQUALITIES std::cerr << " update bound using " << ie << std::endl; std::cerr << " the new bound for " << *term.variable << " is "<< bounds_[term.variable] << std::endl; #endif changed = true; } - if (res == UpdateResult::overflow) { -#ifdef CLINGO_DEBUG_INEQUALITIES - std::cerr << " overflow updating bound of " << *term.variable << std::endl; -#endif - return; - } } } } @@ -410,154 +465,6 @@ void IESolver::add(IEContext &context) { subSolvers_.emplace_front(context, this); } -namespace { - -template -I floordiv(I n, I m) { - using std::div; - auto a = div(n, m); - if (((n < 0) ^ (m < 0)) && a.rem != 0) { - a.quot--; - } - return a.quot; -} - -template -I ceildiv(I n, I m) { - using std::div; - auto a = div(n, m); - if (((n < 0) ^ (m < 0)) && a.rem != 0) { - a.quot++; - } - return a.quot; -} - -template -I div(bool positive, I a, I b) { - return positive ? floordiv(a, b) : ceildiv(a, b); -} - -int clamp_div(bool positive, int64_t a, int64_t b) { - if (a == std::numeric_limits::min() && b == -1) { - return std::numeric_limits::max(); - } - auto c = div(positive, a, b); - if (c > std::numeric_limits::max()) { - return std::numeric_limits::max(); - } - if (c < std::numeric_limits::min()) { - return std::numeric_limits::min(); - } - return static_cast(c); -} - -template -inline bool check_cast(S in, T &out) { - if (sizeof(T) < sizeof(S) && (in < std::numeric_limits::min() || in > std::numeric_limits::max())) { - return false; - } - out = static_cast(in); - return true; -} - -#ifdef __GNUC__ - -template inline bool check_add(S a, S b, S &c) { - return !__builtin_add_overflow(a, b, &c); -} - -template inline bool check_sub(S a, S b, S &c) { - return !__builtin_sub_overflow(a, b, &c); -} - -template inline bool check_mul(S a, S b, S &c) { - return !__builtin_mul_overflow(a, b, &c); -} - -#else - -inline bool check_add(int32_t a, int32_t b, int32_t &c) { - return check_cast(static_cast(a) + b, c); -} - -template inline bool check_add(S a, S b, S &c) { - using U = std::make_unsigned_t; - c = static_cast(static_cast(a) + static_cast(b)); - return (a < 0 || b < 0 || c >= a) && (a >= 0 || b >= 0 || c <= a); -} - -inline bool check_sub(int32_t a, int32_t b, int32_t &c) { - return check_cast(static_cast(a) - b, c); -} - -template inline bool check_sub(S a, S b, S &c) { - using U = std::make_unsigned_t; - c = static_cast(static_cast(a) - static_cast(b)); - return (a < 0 || b >= 0 || c >= a) && (b < 0 || c <= a); -} - -template inline bool check_mul(S a, S b, S &c) { - if (a > 0 && b > 0 && a > std::numeric_limits::max() / b) { - return false; - } - if (a < 0 && b < 0 && b < std::numeric_limits::max() / a) { - return false; - } - if (a > 0 && b < 0 && b < std::numeric_limits::min() / a) { - return false; - } - if (a < 0 && b > 0 && a < std::numeric_limits::min() / b) { - return false; - } - c = a * b; - return true; -} - -#endif - -} // namespace - -IESolver::UpdateResult IESolver::update_bound_(IETerm const &term, int64_t slack, int num_unbounded) { - bool positive = term.coefficient > 0; - auto type = positive ? IEBound::Upper : IEBound::Lower; - if (num_unbounded == 0) { - int64_t val = 0; - if (!check_mul(term.coefficient, bounds_[term.variable].get(type), val)) { - return UpdateResult::overflow; - } - if (!check_add(slack, val, slack)) { - return UpdateResult::overflow; - } - } - else if (num_unbounded > 1 || bounds_[term.variable].isSet(type)) { - return UpdateResult::unchanged; - } - - - auto value = clamp_div(positive, slack, term.coefficient); - if (bounds_[term.variable].refine(positive ? IEBound::Lower : IEBound::Upper, value)) { - return UpdateResult::changed; - } - return UpdateResult::unchanged; -} - -bool IESolver::update_slack_(IETerm const &term, int64_t &slack, int &num_unbounded) { - auto type = term.coefficient > 0 ? IEBound::Upper : IEBound::Lower; - if (bounds_[term.variable].isSet(type)) { - int64_t val = 0; - if (!check_mul(term.coefficient, bounds_[term.variable].get(type), val)) { - return false; - } - if (!check_sub(slack, val, slack)) { - return false; - } - } - else { - ++num_unbounded; - } - return true; -} - // }}} // {{{ definition of GRef @@ -971,7 +878,7 @@ inline int ipow(int a, int b) { return r; } -void add_(IETermVec &terms, int coefficient, VarTerm const *var = nullptr) { +void add_(IETermVec &terms, int64_t coefficient, VarTerm const *var = nullptr) { // NOTE: could use sorting and maybe use inequalities right away for (auto &term : terms) { if (var == term.variable || (term.variable != nullptr && var != nullptr && term.variable->name == var->name)) { @@ -982,7 +889,7 @@ void add_(IETermVec &terms, int coefficient, VarTerm const *var = nullptr) { terms.emplace_back(IETerm{coefficient, var}); } -bool toNum_(IETermVec const &terms, int &res) { +bool toNum_(IETermVec const &terms, int64_t &res) { res = 0; for (auto const &term : terms) { if (term.variable == nullptr) { @@ -1117,7 +1024,8 @@ bool Term::bind(VarSet &bound) const { collect(occs, false); bool ret = false; for (auto &x : occs) { - if ((x.first->bindRef = bound.insert(x.first->name).second)) { + x.first->bindRef = bound.insert(x.first->name).second; + if (x.first->bindRef) { ret = true; } } @@ -2014,7 +1922,8 @@ bool UnOpTerm::addToLinearTerm(IETermVec &terms) const { add_(terms, -term.coefficient, term.variable); } else { - add_(terms, Gringo::eval(UnOp::NEG, term.coefficient)); + // cannot happen because simplify is be called before bound extraction + return false; } } return true; @@ -2261,7 +2170,7 @@ bool BinOpTerm::addToLinearTerm(IETermVec &terms) const { return true; } case BinOp::MUL: { - int num = 0; + int64_t num = 0; if (toNum_(left, num)) { for (auto &term : right) { add_(terms, num * term.coefficient, term.variable); @@ -2282,12 +2191,7 @@ bool BinOpTerm::addToLinearTerm(IETermVec &terms) const { case BinOp::MOD: case BinOp::POW: case BinOp::XOR: { - int numL = 0; - int numR = 0; - if (toNum_(left, numL) && toNum_(right, numR)) { - add_(terms, Gringo::eval(op_, numL, numR)); - return true; - } + // cannot happen because simplify must be called before bound extraction break; } } diff --git a/libgringo/tests/input/program.cc b/libgringo/tests/input/program.cc index 2b0129633..828ee4e99 100644 --- a/libgringo/tests/input/program.cc +++ b/libgringo/tests/input/program.cc @@ -360,7 +360,6 @@ TEST_CASE("input-program", "[input]") { } SECTION("iesolver") { - // no overflow REQUIRE("q(5)." "p(S):-" "#range(Y,0,1);" @@ -381,18 +380,23 @@ TEST_CASE("input-program", "[input]") { "0<=X<=0x7FFFFFFF, " "0<=Y<=0x7FFFFFFF, " "S=0x7FFFFFFF*X+0x7FFFFFFF*Y."))); - // overflow REQUIRE("q(5)." - "p(S):-q(B);" - "#Arith0=S;" - "#Arith0=(((2147483647*X)+(2147483647*Y))+(2147483647*Z));" - "S=(((2147483647*X)+(2147483647*Y))+(2147483647*Z));" - "Z<=2147483647;" + "p(S):-" + "#range(Z,0,1);" + "#range(Y,0,1);" + "#range(X,0,1);" + "#range(S,0,2147483647);" + "#range(#Arith0,0,2147483647);" + "q(B);" "0<=Z;" - "Y<=2147483647;" + "Z<=2147483647;" "0<=Y;" - "X<=2147483647;" + "Y<=2147483647;" "0<=X;" + "X<=2147483647;" + "S=(((2147483647*X)+(2147483647*Y))+(2147483647*Z));" + "#Arith0=(((2147483647*X)+(2147483647*Y))+(2147483647*Z));" + "#Arith0=S;" "S<=B." == rewrite(parse("q(5). " "p(S) :- q(B), " "S<=B, " diff --git a/third_party/CMakeLists.txt b/third_party/CMakeLists.txt index bdc290fe9..57bdd993a 100644 --- a/third_party/CMakeLists.txt +++ b/third_party/CMakeLists.txt @@ -26,3 +26,7 @@ add_library(tl::optional ALIAS optional) add_library(variant INTERFACE) target_include_directories(variant INTERFACE $) add_library(mpark::variant ALIAS variant) + +add_library(wide_integer INTERFACE) +target_include_directories(wide_integer INTERFACE $) +add_library(math::wide_integer ALIAS wide_integer) diff --git a/third_party/wide-integer b/third_party/wide-integer new file mode 160000 index 000000000..4c9711b46 --- /dev/null +++ b/third_party/wide-integer @@ -0,0 +1 @@ +Subproject commit 4c9711b463431c5b64c680444f35183c053be735