From 04d5105bec9922bbc0de82b514af87348e3015c4 Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 21 Jul 2023 16:52:46 +0200 Subject: [PATCH 01/10] consistently store dimension in const variable when used in for loops --- src/pardibaal/DBM.cpp | 179 +++++++++++++++++++++-------------- src/pardibaal/Federation.cpp | 9 +- 2 files changed, 114 insertions(+), 74 deletions(-) diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp index 295b77d..9ea7800 100644 --- a/src/pardibaal/DBM.cpp +++ b/src/pardibaal/DBM.cpp @@ -108,7 +108,9 @@ namespace pardibaal { } relation_t DBM::relation(const DBM &dbm) const { - if (this->dimension() != dbm.dimension()) + const auto dim = this->dimension(); + + if (dim != dbm.dimension()) return relation_t::different(); else if (this->is_empty()) return dbm.is_empty() ? relation_t::equal() : relation_t::subset(); @@ -117,8 +119,8 @@ namespace pardibaal { bool eq = true, sub = true, super = true; - for (dim_t i = 0; i < dimension(); ++i) - for (dim_t j = 0; j < dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) + for (dim_t j = 0; j < dim; ++j) { sub = sub && this->at(i, j) <= dbm.at(i, j); super = super && this->at(i, j) >= dbm.at(i, j); if (!sub && !super) return relation_t::different(); @@ -180,14 +182,15 @@ namespace pardibaal { template bool DBM::is_different(const Federation& fed) const; bool DBM::is_intersecting(const DBM &dbm) const { + const auto dim = this->dimension(); #ifndef NEXCEPTIONS - if (dbm.dimension() != dimension()) + if (dbm.dimension() != this->dimension()) throw(base_error("ERROR: Cannot measure intersection of two dbms with different dimensions. ", - "Got dimensions ", dbm.dimension(), " and ", dimension())); + "Got dimensions ", dbm.dimension(), " and ", dim)); #endif if (this->is_empty() || dbm.is_empty()) return false; - for (dim_t i = 0; i < dimension(); ++i) { - for (dim_t j = 0; j < dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { bound_t b1 = this->at(i, j); bound_t b2 = dbm.at(j, i); @@ -212,7 +215,8 @@ namespace pardibaal { bool DBM::is_unbounded() const { if (is_empty()) return false; - for (dim_t i = 1; i < dimension(); ++i) + const auto dim = this->dimension(); + for (dim_t i = 1; i < dim; ++i) if (not this->at(i, 0).is_inf()) return false; @@ -222,11 +226,11 @@ namespace pardibaal { void DBM::close() { if (_is_closed) return; - const dim_t size = this->dimension(); + const dim_t dim = this->dimension(); - for(dim_t k = 0; k < size; ++k) - for(dim_t i = 0; i < size; ++i) - for(dim_t j = 0; j < size; ++j) + for(dim_t k = 0; k < dim; ++k) + for(dim_t i = 0; i < dim; ++i) + for(dim_t j = 0; j < dim; ++j) _bounds_table.set(i, j, bound_t::min(_bounds_table.at(i, j), _bounds_table.at(i, k) + _bounds_table.at(k, j))); @@ -234,15 +238,17 @@ namespace pardibaal { } void DBM::close_single_bound(dim_t i, dim_t j) { - const dim_t size = this->dimension(); + const dim_t dim = this->dimension(); - for(dim_t k = 0; k < size; ++k) + for(dim_t k = 0; k < dim; ++k) _bounds_table.set(i, j, bound_t::min(_bounds_table.at(i, j), _bounds_table.at(i, k) + _bounds_table.at(k, j))); } void DBM::future() { - for (dim_t i = 1; i < this->dimension(); ++i) + const dim_t dim = this->dimension(); + + for (dim_t i = 1; i < dim; ++i) _bounds_table.set(i, 0, bound_t::inf()); } @@ -251,9 +257,10 @@ namespace pardibaal { } void DBM::past() { - for (dim_t i = 1; i < this->dimension(); ++i) { + const auto dim = this->dimension(); + for (dim_t i = 1; i < dim; ++i) { this->_bounds_table.set(0, i, bound_t::le_zero()); - for (dim_t j = 1; j < this->dimension(); ++j) { + for (dim_t j = 1; j < dim; ++j) { if (this->_bounds_table.at(j, i) < this->_bounds_table.at(0, i)) { this->_bounds_table.set(0, i, this->_bounds_table.at(j, i)); } @@ -272,8 +279,10 @@ namespace pardibaal { if (lower > upper) throw(base_error("ERROR: lower value of delay interval must be smaller than the upper valuer")); #endif + const auto dim = this->dimension(); + if (lower > 0 || upper > 0) { - for (dim_t i = 1; i < this->dimension(); ++i) { + for (dim_t i = 1; i < dim; ++i) { this->set(0, i, this->at(0, i) - lower); // Raise lower bounds this->set(i, 0, this->at(i, 0) + upper); // Raise upper bounds } @@ -285,8 +294,10 @@ namespace pardibaal { _empty_status = EMPTY; else if (g < _bounds_table.at(x, y)) { _bounds_table.set(x, y, g); - for (dim_t i = 0; i < this->dimension(); ++i) { - for (dim_t j = 0; j < this->dimension(); ++j) { + + const auto dim = this->dimension(); + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (_bounds_table.at(i, x) + _bounds_table.at(x, j) < _bounds_table.at(i, j)) _bounds_table.set(i, j, _bounds_table.at(i, x) + _bounds_table.at(x, j)); @@ -307,7 +318,9 @@ namespace pardibaal { } void DBM::free(dim_t x) { - for (dim_t i = 0; i < dimension(); ++i) { + const auto dim = this->dimension(); + + for (dim_t i = 0; i < dim; ++i) { if (i != x) { _bounds_table.set(x, i, bound_t::inf()); _bounds_table.set(i, x, _bounds_table.at(i, 0)); @@ -317,7 +330,9 @@ namespace pardibaal { // x := m void DBM::assign(dim_t x, val_t m) { - for (dim_t i = 0; i < this->dimension(); ++i) { + const auto dim = this->dimension(); + + for (dim_t i = 0; i < dim; ++i) { _bounds_table.set(x, i, bound_t::non_strict(m) + _bounds_table.at(0, i)); _bounds_table.set(i, x, bound_t::non_strict(-m) + _bounds_table.at(i, 0)); } @@ -325,7 +340,9 @@ namespace pardibaal { // x := y void DBM::copy(dim_t x, dim_t y) { - for (dim_t i = 0; i < this->dimension(); ++i) { + const auto dim = this->dimension(); + + for (dim_t i = 0; i < dim; ++i) { if (i != x) { _bounds_table.set(x, i, _bounds_table.at(y, i)); _bounds_table.set(i, x, _bounds_table.at(i, y)); @@ -336,7 +353,9 @@ namespace pardibaal { } void DBM::shift(dim_t x, val_t n) { - for (dim_t i = 0; i < this->dimension(); ++i) { + const auto dim = this->dimension(); + + for (dim_t i = 0; i < dim; ++i) { if (i != x) { this->_bounds_table.set(x, i, this->_bounds_table.at(x, i) + bound_t::non_strict(n)); this->_bounds_table.set(i, x, this->_bounds_table.at(i, x) + bound_t::non_strict(-n)); @@ -348,14 +367,16 @@ namespace pardibaal { // Simple extrapolation from a ceiling for all clocks. void DBM::extrapolate(const std::vector &ceiling) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (this->dimension() != ceiling.size()) + if (dim != ceiling.size()) throw base_error("ERROR: Got max constants vector of size ", ceiling.size(), " but the DBM has ", - this->dimension(), " clocks"); + dim, " clocks"); #endif - for (dim_t i = 0; i < this->dimension(); ++i) { - for (dim_t j = 0; j < this->dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (!this->_bounds_table.at(i, j).is_inf() && this->_bounds_table.at(i, j) > bound_t::non_strict(ceiling[i])){ this->_bounds_table.set(i, j, bound_t::inf()); } @@ -370,17 +391,19 @@ namespace pardibaal { } void DBM::extrapolate_diagonal(const std::vector &ceiling) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (this->dimension() != ceiling.size()) + if (dim != ceiling.size()) throw base_error("ERROR: Got max constants vector of size ", ceiling.size(), " but the DBM has ", - this->dimension(), " clocks"); + dim, " clocks"); #endif DBM D(*this); std::vector> modified_bounds; - for (dim_t i = 0; i < D.dimension(); ++i) { - for (dim_t j = 0; j < D.dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (i == j) continue; if ((D.at(i, j).get_bound() > ceiling[i]) || (-D.at(0, i).get_bound() > ceiling[i]) || @@ -415,15 +438,17 @@ namespace pardibaal { } void DBM::extrapolate_lu(const std::vector &lower, const std::vector &upper) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (this->dimension() != lower.size() || this->dimension() != upper.size()) + if (dim != lower.size() || dim != upper.size()) throw base_error("ERROR: Got LU constants vector of size ", lower.size(), " and ", upper.size(), - " but the DBM has ", this->dimension(), " clocks"); + " but the DBM has ", dim, " clocks"); #endif DBM D(*this); - for (dim_t i = 0; i < D.dimension(); ++i) { - for (dim_t j = 0; j < D.dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (i == j) continue; else if (D.at(i, j).get_bound() > lower[i]) this->set(i, j, bound_t::inf()); @@ -446,15 +471,17 @@ namespace pardibaal { } void DBM::extrapolate_lu_diagonal(const std::vector &lower, const std::vector &upper) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (this->dimension() != lower.size() || this->dimension() != upper.size()) + if (dim != lower.size() || dim != upper.size()) throw base_error("ERROR: Got LU constants vector of size ", lower.size(), " and ", upper.size(), - " but the DBM has ", this->dimension(), " clocks"); + " but the DBM has ", dim, " clocks"); #endif DBM D(*this); - for (dim_t i = 0; i < D.dimension(); ++i) { - for (dim_t j = 0; j < D.dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (i == j) continue; else if ((D.at(i, j).get_bound() > lower[i]) || (-D.at(0, i).get_bound() > -lower[i]) || @@ -479,18 +506,20 @@ namespace pardibaal { } void DBM::intersection(const DBM &dbm) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (dbm.dimension() != dimension()) + if (dbm.dimension() != dim) throw(base_error("ERROR: Cannot take intersection of two dbms with different dimensions. ", - "Got dimensions ", dbm.dimension(), " and ", dimension())); + "Got dimensions ", dbm.dimension(), " and ", dim)); #endif if (dbm.is_empty() || this->is_empty()) { this->_empty_status = EMPTY; return; } - for (dim_t i = 0; i < dimension(); ++i) - for (dim_t j = 0; j < dimension(); ++j) + for (dim_t i = 0; i < dim; ++i) + for (dim_t j = 0; j < dim; ++j) this->_bounds_table.set(i, j, bound_t::min(this->at(i, j), dbm.at(i, j))); _empty_status = UNKNOWN; @@ -499,17 +528,19 @@ namespace pardibaal { } void DBM::remove_clock(dim_t c) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS if (c == 0) throw base_error("ERROR: Cannot remove the zero clock"); - if (c >= this->dimension()) - throw base_error("ERROR: Removing clock ", c, " but the DBM only has clocks from 0 to ", dimension() - 1); + if (c >= dim) + throw base_error("ERROR: Removing clock ", c, " but the DBM only has clocks from 0 to ", dim - 1); #endif - DBM D(dimension() - 1); + DBM D(dim - 1); - for (dim_t i = 0, i2 = 0; i < dimension(); ++i, ++i2) { - for (dim_t j = 0, j2 = 0; j < dimension(); ++j) { - if (i == c && i < dimension() -1) {++i;} + for (dim_t i = 0, i2 = 0; i < dim; ++i, ++i2) { + for (dim_t j = 0, j2 = 0; j < dim; ++j) { + if (i == c && i < dim -1) {++i;} if (j == c || i == c) continue; D._bounds_table.set(i2, j2++, this->at(i, j)); @@ -520,16 +551,18 @@ namespace pardibaal { } void DBM::swap_clocks(dim_t a, dim_t b) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS if (a == 0 || b == 0) throw base_error("ERROR: Cannot swap the zero clock"); - if (a >= this->dimension() || b >= this->dimension()) - throw base_error("ERROR: Swapping clock ", a, " and ", b, " but the DBM only has clocks from 0 to ", dimension() - 1); + if (a >= dim || b >= dim) + throw base_error("ERROR: Swapping clock ", a, " and ", b, " but the DBM only has clocks from 0 to ", dim - 1); #endif if (a == b) return; bound_t tmp; - for (dim_t i = 0; i < dimension(); ++i) { + for (dim_t i = 0; i < dim; ++i) { if (!(i == a || i == b)) { tmp = at(i, a); _bounds_table.set(i, a, at(i, b)); @@ -547,18 +580,20 @@ namespace pardibaal { } void DBM::add_clock_at(dim_t c) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS if (c == 0) throw base_error("ERROR: Cannot add a new clock at index zero"); - if (c > this->dimension()) - throw base_error("ERROR: Adding clock at index", c, " but the DBM only has clocks from 0 to ", dimension() - 1); + if (c > dim) + throw base_error("ERROR: Adding clock at index", c, " but the DBM only has clocks from 0 to ", dim - 1); #endif - DBM D(dimension() + 1); + DBM D(dim + 1); - for (dim_t i = 0, i2 = 0; i < D.dimension(); ++i, ++i2) { - for (dim_t j = 0, j2 = 0; j < D.dimension(); ++j) { - if (i == c && i < D.dimension() - 1) {++i;} + for (dim_t i = 0, i2 = 0; i < dim + 1; ++i, ++i2) { + for (dim_t j = 0, j2 = 0; j < dim + 1; ++j) { + if (i == c && i < dim) {++i;} if (j == c || i == c) continue; D._bounds_table.set(i, j, this->at(i2, j2++)); } @@ -572,10 +607,12 @@ namespace pardibaal { /* assume number of '1' bits in src_bits and dst_bits match, and * that the length of src_bits is the same as _number_of_clocks */ + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (src_bits.size() != this->dimension()) + if (src_bits.size() != dim) throw base_error("ERROR: src_bits has size: ", src_bits.size(), " but the dimension of the DBM is: ", - this->dimension(), " but they must be equal"); + dim, " but they must be equal"); int src = std::count_if(dst_bits.begin(), dst_bits.end(), [](bool b){return b;}); int dst = std::count_if(src_bits.begin(), src_bits.end(), [](bool b){return b;}); @@ -588,7 +625,7 @@ namespace pardibaal { std::vector src_indir(src_bits.size(), 0); dim_t dst_cnt = 0; - for (dim_t i = 0; i < src_bits.size(); ++i) { + for (dim_t i = 0; i < dim; ++i) { if (src_bits[i]) { while (not dst_bits[dst_cnt]) ++dst_cnt; // increment to first used position src_indir[i] = dst_cnt++; @@ -598,8 +635,8 @@ namespace pardibaal { } // dest(src_indir[i], src_indir[j] = src(i, j); - for (dim_t i = 0; i < src_indir.size(); ++i) { - for (dim_t j = 0; j < src_indir.size(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (src_indir[i] != -1 && src_indir[j] != -1) dest_dbm._bounds_table.set(src_indir[i], src_indir[j], this->_bounds_table.at(i, j)); } @@ -616,15 +653,17 @@ namespace pardibaal { } void DBM::reorder(const std::vector& order, dim_t new_size) { + const auto dim = this->dimension(); + #ifndef NEXCEPTIONS - if (order.size() != this->dimension()) + if (order.size() != dim) throw base_error("ERROR: Order vector has size: ", order.size(), " but the dimension of the DBM is: ", - this->dimension(), " They must be equal"); + dim, " They must be equal"); int clocks_removed = std::count_if(order.begin(), order.end(), [](dim_t i){return i == ~0;}); - if (this->dimension() - clocks_removed != new_size) + if (dim - clocks_removed != new_size) throw base_error("ERROR: new_size does not match the number of clocks removed. new_size is: ", new_size, - " current size: ", this->dimension(), " Clocks removed: ", clocks_removed); + " current size: ", dim, " Clocks removed: ", clocks_removed); for (const dim_t& i : order) if (i >= new_size && i != (dim_t) -1) throw base_error("ERROR: order has value ", order[i], " on index ", i, @@ -633,8 +672,8 @@ namespace pardibaal { DBM D(new_size); - for (dim_t i = 0; i < this->dimension(); ++i) { - for (dim_t j = 0; j < this->dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { if (order[i] != ~0 && order[j] != ~0) D._bounds_table.set(order[i], order[j], this->_bounds_table.at(i, j)); } diff --git a/src/pardibaal/Federation.cpp b/src/pardibaal/Federation.cpp index e9d964a..5d76258 100644 --- a/src/pardibaal/Federation.cpp +++ b/src/pardibaal/Federation.cpp @@ -84,17 +84,18 @@ namespace pardibaal { } void Federation::subtract(const DBM& dbm) { + const auto dim = this->dimension(); #ifndef NEXCEPTIONS if (!zones.empty()) { - if (dimension() != dbm.dimension()) + if (dim != dbm.dimension()) throw base_error("ERROR: Subtracting dbm with dimension: ", dbm.dimension(), - " from a federation with dimension: ", dimension()); + " from a federation with dimension: ", dim); } #endif auto fed = Federation(); for (auto z : zones) { - for (dim_t i = 0; i < dimension(); ++i) { - for (dim_t j = 0; j < dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { // This check ensures that the zone added is non-empty iff it is on max canonical form. if (z.at(i, j) > dbm.at(i, j)) { z.restrict(j, i, bound_t(-dbm.at(i, j).get_bound(), dbm.at(i, j).is_non_strict())); From e4465b4fcd89ef181e6ff3ad60a7a1029ad3c4be Mon Sep 17 00:00:00 2001 From: Thomas Date: Mon, 24 Jul 2023 16:16:37 +0200 Subject: [PATCH 02/10] Bounds to 32 bits, added overflow checks and inlined some methods --- src/pardibaal/bound_t.cpp | 78 +++++++++++++---------------------- src/pardibaal/bound_t.h | 85 +++++++++++++++++++++++---------------- 2 files changed, 80 insertions(+), 83 deletions(-) diff --git a/src/pardibaal/bound_t.cpp b/src/pardibaal/bound_t.cpp index d216e7d..7baa44a 100644 --- a/src/pardibaal/bound_t.cpp +++ b/src/pardibaal/bound_t.cpp @@ -21,79 +21,59 @@ */ #include +#include #include "bound_t.h" namespace pardibaal { - // val_t bound_t::get_bound() const {return this->_n;} - // bool bound_t::is_strict() const {return this->_strict;} - // bool bound_t::is_non_strict() const {return not this->_strict;} - // bool bound_t::is_inf() const {return this->_inf;} - - const bound_t &bound_t::max(const bound_t &a, const bound_t &b) {return a < b ? b : a;} - bound_t bound_t::max(bound_t &&a, bound_t &&b) {return max(a, b);} - bound_t bound_t::max(const bound_t &a, bound_t &&b) {return max(a, b);} - bound_t bound_t::max(bound_t &&a, const bound_t &b) {return max(a, b);} - - const bound_t &bound_t::min(const bound_t &a, const bound_t &b) {return a <= b ? a : b;} - bound_t bound_t::min(bound_t &&a, bound_t &&b) {return bound_t::min(a, b);} - bound_t bound_t::min(const bound_t &a, bound_t &&b) {return bound_t::min(a, b);} - bound_t bound_t::min(bound_t &&a, const bound_t &b) {return bound_t::min(a, b);} - bound_t bound_t::operator+(bound_t rhs) const { + if (this->is_inf() || rhs.is_inf()) return bound_t::inf(); + assert(get_bound() < BOUND_VAL_MAX - rhs.get_bound() && "Overflow"); + return bound_t(this->get_bound() + rhs.get_bound(), this->is_strict() || rhs.is_strict()); } bound_t bound_t::operator+(val_t rhs) const { - if (not this->is_inf()) - return bound_t(this->get_bound() + rhs, this->is_strict()); - return *this; - } + if (this->is_inf()) + return *this; - bound_t bound_t::operator-(val_t rhs) const { - if (not this->is_inf()) - return bound_t(this->get_bound() - rhs, this->is_strict()); - return *this; - } + assert(get_bound() < BOUND_VAL_MAX - rhs && "Overflow"); - bound_t bound_t::operator*(val_t rhs) const { - if (not this->is_inf()) - return bound_t(this->get_bound() * rhs, this->is_strict()); - return *this; + return bound_t(this->get_bound() + rhs, this->is_strict()); } - bool bound_t::operator<(bound_t rhs) const { - if (this->is_inf()) return false; - if (rhs.is_inf()) return true; + bound_t bound_t::operator-(val_t rhs) const { + if (this->is_inf()) + return *this; - if (this->get_bound() == rhs.get_bound()) - return !rhs.is_strict() && this->is_strict(); + assert(get_bound() > BOUND_VAL_MIN + rhs && rhs > BOUND_VAL_MIN && rhs < BOUND_VAL_MAX && "Underflow"); - return this->get_bound() < rhs.get_bound(); + return bound_t(this->get_bound() - rhs, this->is_strict()); } - bool bound_t::operator==(bound_t rhs) const { - if (this->is_inf() || rhs.is_inf()) - return this->is_inf() && rhs.is_inf(); + bound_t bound_t::operator*(val_t rhs) const { + if (this->is_inf()) + return *this; + + auto prod = this->get_bound() * rhs; + + assert((this->get_bound() != 0 && prod / this->get_bound() != rhs) + && prod > BOUND_VAL_MIN && prod < BOUND_VAL_MAX + && rhs > BOUND_VAL_MIN && rhs < BOUND_VAL_MAX && ("Overflow or Underflow")); - return (this->get_bound() == rhs.get_bound()) && (this->is_strict() == rhs.is_strict()); + return bound_t(this->get_bound() * rhs, this->is_strict()); } - bool bound_t::operator!=(bound_t rhs) const {return not (*this == rhs);} - bool bound_t::operator>(bound_t rhs) const {return rhs < *this;} - bool bound_t::operator>=(bound_t rhs) const {return not (*this < rhs);} - bool bound_t::operator<=(bound_t rhs) const {return not (rhs < *this);} - - bool bound_t::operator==(val_t rhs) const {return *this == bound_t::non_strict(rhs);} - bool bound_t::operator!=(val_t rhs) const {return *this != bound_t::non_strict(rhs);} - bool bound_t::operator<(val_t rhs) const {return *this < bound_t::non_strict(rhs);} - bool bound_t::operator>(val_t rhs) const {return *this > bound_t::non_strict(rhs);} - bool bound_t::operator<=(val_t rhs) const {return *this <= bound_t::non_strict(rhs);} - bool bound_t::operator>=(val_t rhs) const {return *this >= bound_t::non_strict(rhs);} + bool bound_t::operator==(val_t rhs) const {return this->_data == bound_t::non_strict(rhs)._data;} + bool bound_t::operator!=(val_t rhs) const {return this->_data != bound_t::non_strict(rhs)._data;} + bool bound_t::operator<(val_t rhs) const {return this->_data < bound_t::non_strict(rhs)._data;} + bool bound_t::operator>(val_t rhs) const {return this->_data > bound_t::non_strict(rhs)._data;} + bool bound_t::operator<=(val_t rhs) const {return this->_data <= bound_t::non_strict(rhs)._data;} + bool bound_t::operator>=(val_t rhs) const {return this->_data >= bound_t::non_strict(rhs)._data;} bool lt(bound_t lhs, bound_t rhs) {return lhs < rhs;} bool le(bound_t lhs, bound_t rhs) {return lhs <= rhs;} diff --git a/src/pardibaal/bound_t.h b/src/pardibaal/bound_t.h index 50d1237..2a754f9 100644 --- a/src/pardibaal/bound_t.h +++ b/src/pardibaal/bound_t.h @@ -25,46 +25,64 @@ #include #include +#include namespace pardibaal { using dim_t = uint32_t; using val_t = int32_t; + /** + * Representing a bound in 32 bit: + * Least significant bit is strictness, 1 means non strict and 0 means strict. + * the 31 most significant bits are right shifted (preserving signed bit) and read as 32 bit signed int. + * Infinite bound is represented as the largesst 31 bit value. + * This means that the max limit for a bound value is a 32 bit int where the two most significant bits are 0 + */ + const int32_t INF_BOUND = std::numeric_limits::max(); + const int32_t LE_ZERO_BOUND = 1; + const int32_t LT_ZERO_BOUND = 0; + const int32_t BOUND_VAL_MAX = std::numeric_limits::max() >> 1; + const int32_t BOUND_VAL_MIN = std::numeric_limits::min() >> 1; + enum strict_e {STRICT, NON_STRICT}; struct bound_t { + private: - val_t _n = 0; - bool _strict = false, - _inf = false; + val_t _data = LE_ZERO_BOUND; + + constexpr bound_t(val_t bound) : _data(bound) {} - constexpr bound_t(val_t n, bool strict, bool inf) : _n(n), _strict(strict), _inf(inf){}; public: constexpr bound_t(){}; - constexpr bound_t(val_t n, strict_e strictness) : _n(n) {_strict = strictness == STRICT ? true : false;} - constexpr bound_t(val_t n, bool strict) : _n(n), _strict(strict) {} - - [[nodiscard]] static constexpr bound_t strict(val_t n) {return bound_t(n, true, false);} - [[nodiscard]] static constexpr bound_t non_strict(val_t n) {return bound_t(n, false, false);} - [[nodiscard]] static constexpr bound_t inf() {return bound_t(0, true, true);} - [[nodiscard]] static constexpr bound_t le_zero() {return bound_t(0, false, false);} - [[nodiscard]] static constexpr bound_t lt_zero() {return bound_t(0, true, false);} - - [[nodiscard]] inline val_t get_bound() const {return this->_n;} - [[nodiscard]] inline bool is_strict() const {return this->_strict;} - [[nodiscard]] inline bool is_non_strict() const {return not this->_strict;} - [[nodiscard]] inline bool is_inf() const {return this->_inf;} - - [[nodiscard]] static const bound_t& max(const bound_t &a, const bound_t &b); - [[nodiscard]] static bound_t max(bound_t &&a, bound_t &&b); - [[nodiscard]] static bound_t max(const bound_t &a, bound_t &&b); - [[nodiscard]] static bound_t max(bound_t &&a, const bound_t &b); - - [[nodiscard]] static const bound_t& min(const bound_t &a, const bound_t &b); - [[nodiscard]] static bound_t min(bound_t &&a, bound_t &&b); - [[nodiscard]] static bound_t min(const bound_t &a, bound_t &&b); - [[nodiscard]] static bound_t min(bound_t &&a, const bound_t &b); + constexpr bound_t(val_t n, strict_e strictness) { + if (strictness == STRICT) + _data = n << 1; + else + _data = ~((~n) << 1); + } + + constexpr bound_t(val_t n, bool strict) { + if (strict) + _data = n << 1; + else + _data = ~((~n) << 1); + } + + [[nodiscard]] static constexpr bound_t strict(val_t n) {return bound_t(n << 1);} + [[nodiscard]] static constexpr bound_t non_strict(val_t n) {return bound_t(~((~n) << 1));} + [[nodiscard]] static constexpr bound_t inf() {return bound_t(INF_BOUND);} + [[nodiscard]] static constexpr bound_t le_zero() {return bound_t(LE_ZERO_BOUND);} + [[nodiscard]] static constexpr bound_t lt_zero() {return bound_t(LT_ZERO_BOUND);} + + [[nodiscard]] inline val_t get_bound() const {return this->_data >> 1;} + [[nodiscard]] inline bool is_strict() const {return not this->is_non_strict();} + [[nodiscard]] inline bool is_non_strict() const {return this->_data << 31;} + [[nodiscard]] inline bool is_inf() const {return this->_data & INF_BOUND;} + + [[nodiscard]] static inline bound_t max(bound_t a, bound_t b) {return a < b ? b : a;} + [[nodiscard]] static inline bound_t min(bound_t a, bound_t b) {return a < b ? a : b;} [[nodiscard]] bound_t operator+(bound_t rhs) const; [[nodiscard]] bound_t operator+(val_t rhs) const; @@ -73,13 +91,12 @@ namespace pardibaal { [[nodiscard]] bound_t operator*(val_t rhs) const; - [[nodiscard]] bool operator<(bound_t rhs) const; - [[nodiscard]] bool operator==(bound_t rhs) const; - - [[nodiscard]] bool operator!=(bound_t rhs) const; - [[nodiscard]] bool operator>(bound_t rhs) const; - [[nodiscard]] bool operator>=(bound_t rhs) const; - [[nodiscard]] bool operator<=(bound_t rhs) const; + [[nodiscard]] inline bool operator==(bound_t rhs) const {return this->_data == rhs._data;} + [[nodiscard]] inline bool operator!=(bound_t rhs) const {return this->_data != rhs._data;} + [[nodiscard]] inline bool operator<(bound_t rhs) const {return this->_data < rhs._data;} + [[nodiscard]] inline bool operator>(bound_t rhs) const {return this->_data > rhs._data;} + [[nodiscard]] inline bool operator>=(bound_t rhs) const {return this->_data >= rhs._data;} + [[nodiscard]] inline bool operator<=(bound_t rhs) const {return this->_data <= rhs._data;} [[nodiscard]] bool operator==(val_t rhs) const; [[nodiscard]] bool operator!=(val_t rhs) const; From 4a1cb42120829ba95b4e6183da3104a98a5dd861 Mon Sep 17 00:00:00 2001 From: Thomas Date: Thu, 27 Jul 2023 11:30:36 +0200 Subject: [PATCH 03/10] fixed unnecessary checks in tests and overflow check in bound_t * int --- src/pardibaal/bound_t.cpp | 2 +- src/pardibaal/bound_t.h | 2 +- test/DBM_test.cpp | 4 ++-- test/bound_test.cpp | 8 ++++---- test/difference_bound_test.cpp | 2 +- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/pardibaal/bound_t.cpp b/src/pardibaal/bound_t.cpp index 7baa44a..7443600 100644 --- a/src/pardibaal/bound_t.cpp +++ b/src/pardibaal/bound_t.cpp @@ -61,7 +61,7 @@ namespace pardibaal { auto prod = this->get_bound() * rhs; - assert((this->get_bound() != 0 && prod / this->get_bound() != rhs) + assert((!(this->get_bound() != 0) || (prod / this->get_bound() == rhs)) && prod > BOUND_VAL_MIN && prod < BOUND_VAL_MAX && rhs > BOUND_VAL_MIN && rhs < BOUND_VAL_MAX && ("Overflow or Underflow")); diff --git a/src/pardibaal/bound_t.h b/src/pardibaal/bound_t.h index 2a754f9..f8f08b3 100644 --- a/src/pardibaal/bound_t.h +++ b/src/pardibaal/bound_t.h @@ -79,7 +79,7 @@ namespace pardibaal { [[nodiscard]] inline val_t get_bound() const {return this->_data >> 1;} [[nodiscard]] inline bool is_strict() const {return not this->is_non_strict();} [[nodiscard]] inline bool is_non_strict() const {return this->_data << 31;} - [[nodiscard]] inline bool is_inf() const {return this->_data & INF_BOUND;} + [[nodiscard]] inline bool is_inf() const {return this->_data == INF_BOUND;} [[nodiscard]] static inline bound_t max(bound_t a, bound_t b) {return a < b ? b : a;} [[nodiscard]] static inline bound_t min(bound_t a, bound_t b) {return a < b ? a : b;} diff --git a/test/DBM_test.cpp b/test/DBM_test.cpp index 892f7b0..2665714 100644 --- a/test/DBM_test.cpp +++ b/test/DBM_test.cpp @@ -93,12 +93,12 @@ BOOST_AUTO_TEST_CASE(bounded_future_test_3) { for (dim_t j = 0; j < 10; j++) { if (j == 0 && i != 0) { if (i == 2) - BOOST_CHECK(D.at(i, j) == bound_t::inf() && D.at(i,j).get_bound() == 0); + BOOST_CHECK(D.at(i, j) == bound_t::inf()); else BOOST_CHECK(D.at(i, j) == bound_t::non_strict(5)); } else { if (i == 2 && j != 2) - BOOST_CHECK(D.at(i, j) == bound_t::inf() && D.at(i, j).get_bound() == 0); + BOOST_CHECK(D.at(i, j) == bound_t::inf()); else BOOST_CHECK(D.at(i, j) == bound_t::le_zero()); } diff --git a/test/bound_test.cpp b/test/bound_test.cpp index 478b841..5e242e5 100644 --- a/test/bound_test.cpp +++ b/test/bound_test.cpp @@ -147,7 +147,7 @@ BOOST_AUTO_TEST_CASE(add_test_5) { BOOST_CHECK(a + 5 == b); BOOST_CHECK(b == bound_t::inf()); - BOOST_CHECK(b.get_bound() == 0); + // BOOST_CHECK(b.get_bound() == 0); } BOOST_AUTO_TEST_CASE(add_test_6) { @@ -178,7 +178,7 @@ BOOST_AUTO_TEST_CASE(subtract_test_3) { auto b = a - 5; BOOST_CHECK(b == bound_t::inf()); - BOOST_CHECK(b.get_bound() == 0); + // BOOST_CHECK(b.get_bound() == 0); } BOOST_AUTO_TEST_CASE(multiply_test_1) { @@ -193,7 +193,7 @@ BOOST_AUTO_TEST_CASE(multiply_test_2) { auto b = a * 5; BOOST_CHECK(b == bound_t::inf()); - BOOST_CHECK(b.get_bound() == 0); + // BOOST_CHECK(b.get_bound() == 0); } BOOST_AUTO_TEST_CASE(comp_test_6) { @@ -302,4 +302,4 @@ BOOST_AUTO_TEST_CASE(comp_test_14) { BOOST_CHECK(a > b); BOOST_CHECK(!(a <= b)); BOOST_CHECK(a >= b); -} +} \ No newline at end of file diff --git a/test/difference_bound_test.cpp b/test/difference_bound_test.cpp index 19a57d5..f467199 100644 --- a/test/difference_bound_test.cpp +++ b/test/difference_bound_test.cpp @@ -43,7 +43,7 @@ BOOST_AUTO_TEST_CASE(inf_test_1) { BOOST_CHECK(c._i == 10); BOOST_CHECK(c._j == 3); - BOOST_CHECK(c._bound.is_strict()); + BOOST_CHECK(c._bound.is_non_strict()); BOOST_CHECK(c._bound.is_inf()); } From c38513eb835e2676e054cf42b15e360883ead658 Mon Sep 17 00:00:00 2001 From: Thomas Date: Thu, 27 Jul 2023 13:35:19 +0200 Subject: [PATCH 04/10] use more efficient constructor/operations in bound_t operators --- src/pardibaal/bound_t.cpp | 29 +++++++++++++++++++++-------- src/pardibaal/bound_t.h | 12 +++--------- 2 files changed, 24 insertions(+), 17 deletions(-) diff --git a/src/pardibaal/bound_t.cpp b/src/pardibaal/bound_t.cpp index 7443600..0605ac1 100644 --- a/src/pardibaal/bound_t.cpp +++ b/src/pardibaal/bound_t.cpp @@ -33,8 +33,14 @@ namespace pardibaal { return bound_t::inf(); assert(get_bound() < BOUND_VAL_MAX - rhs.get_bound() && "Overflow"); + + const val_t val1 = this->_data, + val2 = rhs._data; + + // If both are non-strict (first bit is 1), then the result should be non strict + const val_t strictness = 1 & val1 & val2; - return bound_t(this->get_bound() + rhs.get_bound(), this->is_strict() || rhs.is_strict()); + return bound_t((((val1 >> 1) + (val2 >> 1)) << 1) | strictness); } bound_t bound_t::operator+(val_t rhs) const { @@ -42,8 +48,11 @@ namespace pardibaal { return *this; assert(get_bound() < BOUND_VAL_MAX - rhs && "Overflow"); + + const val_t lhs = this->_data; + const val_t strictness = 1 & lhs; - return bound_t(this->get_bound() + rhs, this->is_strict()); + return bound_t((((lhs >> 1) + rhs) << 1) | strictness); } bound_t bound_t::operator-(val_t rhs) const { @@ -52,20 +61,24 @@ namespace pardibaal { assert(get_bound() > BOUND_VAL_MIN + rhs && rhs > BOUND_VAL_MIN && rhs < BOUND_VAL_MAX && "Underflow"); - return bound_t(this->get_bound() - rhs, this->is_strict()); + const val_t lhs = this->_data; + const val_t strictness = 1 & lhs; + + return bound_t((((lhs >> 1) - rhs) << 1) | strictness); } bound_t bound_t::operator*(val_t rhs) const { if (this->is_inf()) return *this; - - auto prod = this->get_bound() * rhs; - assert((!(this->get_bound() != 0) || (prod / this->get_bound() == rhs)) - && prod > BOUND_VAL_MIN && prod < BOUND_VAL_MAX + assert((!(this->get_bound() != 0) || (this->get_bound() * rhs / this->get_bound() == rhs)) + && this->get_bound() * rhs > BOUND_VAL_MIN && this->get_bound() * rhs < BOUND_VAL_MAX && rhs > BOUND_VAL_MIN && rhs < BOUND_VAL_MAX && ("Overflow or Underflow")); - return bound_t(this->get_bound() * rhs, this->is_strict()); + const val_t lhs = this->_data; + const val_t strictness = 1 & lhs; + + return bound_t((((lhs >> 1) * rhs) << 1) | strictness); } bool bound_t::operator==(val_t rhs) const {return this->_data == bound_t::non_strict(rhs)._data;} diff --git a/src/pardibaal/bound_t.h b/src/pardibaal/bound_t.h index f8f08b3..f152cee 100644 --- a/src/pardibaal/bound_t.h +++ b/src/pardibaal/bound_t.h @@ -45,7 +45,7 @@ namespace pardibaal { const int32_t BOUND_VAL_MAX = std::numeric_limits::max() >> 1; const int32_t BOUND_VAL_MIN = std::numeric_limits::min() >> 1; - enum strict_e {STRICT, NON_STRICT}; + enum strict_e {STRICT = 0, NON_STRICT = 1}; struct bound_t { @@ -57,17 +57,11 @@ namespace pardibaal { public: constexpr bound_t(){}; constexpr bound_t(val_t n, strict_e strictness) { - if (strictness == STRICT) - _data = n << 1; - else - _data = ~((~n) << 1); + _data = (n << 1) | (val_t) strictness; } constexpr bound_t(val_t n, bool strict) { - if (strict) - _data = n << 1; - else - _data = ~((~n) << 1); + _data = (n << 1) | (val_t) !strict; } [[nodiscard]] static constexpr bound_t strict(val_t n) {return bound_t(n << 1);} From f0841a85c95d0aaee7fee42fea349ab9b71dbf6d Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 28 Jul 2023 17:23:08 +0200 Subject: [PATCH 05/10] remove dbm copy from diagonal extrapolation --- src/pardibaal/DBM.cpp | 44 +++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp index 9ea7800..5909dff 100644 --- a/src/pardibaal/DBM.cpp +++ b/src/pardibaal/DBM.cpp @@ -398,43 +398,43 @@ namespace pardibaal { throw base_error("ERROR: Got max constants vector of size ", ceiling.size(), " but the DBM has ", dim, " clocks"); #endif - DBM D(*this); std::vector> modified_bounds; + modified_bounds.reserve(dim * (dim - 1)); - for (dim_t i = 0; i < dim; ++i) { + for (dim_t oi = 1; oi <= dim; ++oi) { + auto i = oi % dim; // Ordering: 1, 2, ..., dim, 0. for (dim_t j = 0; j < dim; ++j) { if (i == j) continue; - if ((D.at(i, j).get_bound() > ceiling[i]) || - (-D.at(0, i).get_bound() > ceiling[i]) || - (-D.at(0, j).get_bound() > ceiling[j] && i != 0)) { - this->set(i, j, bound_t::inf()); + auto bound_ij = _bounds_table.at(i, j).get_bound(); + + if((- _bounds_table.at(0, i).get_bound() > ceiling[i])) { + this->_bounds_table.set(i, j, bound_t::inf()); modified_bounds.push_back({i, j}); } - else if (-D.at(i, j).get_bound() > ceiling[j] && i == 0) { - this->set(i, j, bound_t::strict(-ceiling[j])); + else if ((i != 0 && -_bounds_table.at(0, j).get_bound() > ceiling[j])) { + this->_bounds_table.set(i, j, bound_t::inf()); modified_bounds.push_back({i, j}); } - - // Make sure we don't set 0, j to positive bound or i, 0 to a negative one - //TODO: We only do this because regular close() does not catch these. - // We should propably use a smarter close() - if (i == 0 && this->at(i, j) > bound_t::le_zero()) { - this->set(i, j, bound_t::le_zero()); + else if (bound_ij > ceiling[i]) { + this->_bounds_table.set(i, j, bound_t::inf()); + modified_bounds.push_back({i, j}); } - if (j == 0 && this->at(i, j) < bound_t::le_zero()) { - this->set(i, j, bound_t::le_zero()); + else if (-bound_ij > ceiling[j] && i == 0) { + // If it is the case that ceiling is -INF, then we should not do anything + this->_bounds_table.set(i, j, bound_t::strict(-ceiling[j])); + modified_bounds.push_back({i, j}); } + // Make sure we don't set 0, j to positive bound + if ((i == 0 && _bounds_table.at(i, j) > bound_t::le_zero())) { + this->_bounds_table.set(i, j, bound_t::le_zero()); + } } } - for (const auto& bound : modified_bounds) - close_single_bound(bound.first, bound.second); - - //TODO: Do something smart where we only close if something changes - // _is_closed = false; - // this->close(); + for (const auto b : modified_bounds) + close_single_bound(b.first, b.second); } void DBM::extrapolate_lu(const std::vector &lower, const std::vector &upper) { From 9a9c8bdf23a58072258b7cebbf6099736b8106ac Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 28 Jul 2023 17:36:00 +0200 Subject: [PATCH 06/10] close only necessary bounds --- src/pardibaal/DBM.cpp | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp index 5909dff..c3135fb 100644 --- a/src/pardibaal/DBM.cpp +++ b/src/pardibaal/DBM.cpp @@ -402,6 +402,10 @@ namespace pardibaal { std::vector> modified_bounds; modified_bounds.reserve(dim * (dim - 1)); + std::vector close_zero(dim, false); + + std::vector skip(dim, false); + for (dim_t oi = 1; oi <= dim; ++oi) { auto i = oi % dim; // Ordering: 1, 2, ..., dim, 0. for (dim_t j = 0; j < dim; ++j) { @@ -410,11 +414,11 @@ namespace pardibaal { if((- _bounds_table.at(0, i).get_bound() > ceiling[i])) { this->_bounds_table.set(i, j, bound_t::inf()); - modified_bounds.push_back({i, j}); + skip[i] = true; } else if ((i != 0 && -_bounds_table.at(0, j).get_bound() > ceiling[j])) { this->_bounds_table.set(i, j, bound_t::inf()); - modified_bounds.push_back({i, j}); + close_zero[j] = true; } else if (bound_ij > ceiling[i]) { this->_bounds_table.set(i, j, bound_t::inf()); @@ -433,8 +437,15 @@ namespace pardibaal { } } - for (const auto b : modified_bounds) - close_single_bound(b.first, b.second); + for (dim_t j = 0; j < dim; ++j) + if(close_zero[j]) + for (dim_t i = 0; i < dim; ++i) + _bounds_table.set(i, j, bound_t::min(_bounds_table.at(i, j), _bounds_table.at(i, 0) + _bounds_table.at(0, j))); + + for (dim_t k = 0; k < dim; ++k) + if (not skip[k]) + for (const auto& b : modified_bounds) + _bounds_table.set(b.first, b.second, bound_t::min(_bounds_table.at(b.first, b.second), _bounds_table.at(b.first, k) + _bounds_table.at(k, b.second))); } void DBM::extrapolate_lu(const std::vector &lower, const std::vector &upper) { From 6f2e627910e8318c85af049c9a4cecb67ee896dc Mon Sep 17 00:00:00 2001 From: Thomas Date: Sun, 30 Jul 2023 13:43:41 +0200 Subject: [PATCH 07/10] remove dimension call in dbm::is_empty --- src/pardibaal/DBM.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp index c3135fb..31dec26 100644 --- a/src/pardibaal/DBM.cpp +++ b/src/pardibaal/DBM.cpp @@ -76,9 +76,11 @@ namespace pardibaal { if (_empty_status != UNKNOWN) return _empty_status == EMPTY ? true : false; + const dim_t dim = this->dimension(); + // The DBM has to be closed for this to actually work - for (dim_t i = 0; i < this->dimension(); ++i) { - for (dim_t j = 0; j < this->dimension(); ++j) { + for (dim_t i = 0; i < dim; ++i) { + for (dim_t j = 0; j < dim; ++j) { bound_t i_to_j_to_i = this->_bounds_table.at(i, j) + this->_bounds_table.at(j, i); if (i_to_j_to_i < bound_t::le_zero()) { From 57fbe399f33e96abbdbf583696acb067ec8d2e40 Mon Sep 17 00:00:00 2001 From: Thomas Date: Fri, 29 Sep 2023 11:19:55 +0200 Subject: [PATCH 08/10] remove close_zero, add early termination in closure after diag-ext. --- src/pardibaal/DBM.cpp | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp index 01c1eec..73b41b2 100644 --- a/src/pardibaal/DBM.cpp +++ b/src/pardibaal/DBM.cpp @@ -388,9 +388,8 @@ namespace pardibaal { std::vector> modified_bounds; modified_bounds.reserve(dim * (dim - 1)); - std::vector close_zero(dim, false); - std::vector skip(dim, false); + dim_t skip_counter = 0; for (dim_t oi = 1; oi <= dim; ++oi) { auto i = oi % dim; // Ordering: 1, 2, ..., dim, 0. @@ -399,12 +398,14 @@ namespace pardibaal { auto bound_ij = _bounds_table.at(i, j).get_bound(); if((- _bounds_table.at(0, i).get_bound() > ceiling[i])) { - this->_bounds_table.set(i, j, bound_t::inf()); + for (; j < dim; ++j) // Complete j loop and add i to skip only once + if (i != j) + this->_bounds_table.set(i, j, bound_t::inf()); skip[i] = true; + ++skip_counter; } else if ((i != 0 && -_bounds_table.at(0, j).get_bound() > ceiling[j])) { this->_bounds_table.set(i, j, bound_t::inf()); - close_zero[j] = true; } else if (bound_ij > ceiling[i]) { this->_bounds_table.set(i, j, bound_t::inf()); @@ -423,15 +424,21 @@ namespace pardibaal { } } - for (dim_t j = 0; j < dim; ++j) - if(close_zero[j]) - for (dim_t i = 0; i < dim; ++i) - _bounds_table.set(i, j, bound_t::min(_bounds_table.at(i, j), _bounds_table.at(i, 0) + _bounds_table.at(0, j))); + if (skip_counter == dim - 1) // All but the lower bounds are inf. Nothing to close. + return; - for (dim_t k = 0; k < dim; ++k) + // close only first case for k = 0 + for (const auto& b : modified_bounds) + _bounds_table.set(b.first, b.second, bound_t::min(_bounds_table.at(b.first, b.second), _bounds_table.at(b.first, 0) + _bounds_table.at(0, b.second))); + + for (dim_t k = 1; k < dim; ++k) if (not skip[k]) for (const auto& b : modified_bounds) _bounds_table.set(b.first, b.second, bound_t::min(_bounds_table.at(b.first, b.second), _bounds_table.at(b.first, k) + _bounds_table.at(k, b.second))); + else + for (dim_t i = 1; i < dim; ++i) + if (i != k && not skip[i]) + _bounds_table.set(i, k, bound_t::min(_bounds_table.at(i, k), _bounds_table.at(i, 0) + _bounds_table.at(0, k))); } void DBM::extrapolate_lu(const std::vector &lower, const std::vector &upper) { From 14fc1a61a648dd4037907b47c2844f7bd33feb11 Mon Sep 17 00:00:00 2001 From: Thomas Date: Mon, 4 Mar 2024 14:09:30 +0100 Subject: [PATCH 09/10] fix negation error in diagonal LU extrapolation --- src/pardibaal/DBM.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp index 73b41b2..f7824ad 100644 --- a/src/pardibaal/DBM.cpp +++ b/src/pardibaal/DBM.cpp @@ -488,8 +488,8 @@ namespace pardibaal { for (dim_t j = 0; j < dim; ++j) { if (i == j) continue; else if ((D.at(i, j).get_bound() > lower[i]) || - (-D.at(0, i).get_bound() > -lower[i]) || - (-D.at(0, j).get_bound() > -upper[j] && i != 0)) + (-D.at(0, i).get_bound() > lower[i]) || + (-D.at(0, j).get_bound() > upper[j] && i != 0)) this->set(i, j, bound_t::inf()); else if (-D.at(0, j).get_bound() > upper[j] && i == 0) this->set(i, j, bound_t::strict(-upper[j])); From e20dcff97ad638327b687e91069830246e0e438b Mon Sep 17 00:00:00 2001 From: Thomas Date: Mon, 4 Mar 2024 14:38:58 +0100 Subject: [PATCH 10/10] Add test for diagonal LU extrapolate fix --- test/DBM_test.cpp | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/test/DBM_test.cpp b/test/DBM_test.cpp index 2665714..d89441b 100644 --- a/test/DBM_test.cpp +++ b/test/DBM_test.cpp @@ -837,6 +837,28 @@ BOOST_AUTO_TEST_CASE(extrapolate_lu_diagonal_test_1) { BOOST_CHECK(D.at(2, 2) == bound_t::le_zero()); } +BOOST_AUTO_TEST_CASE(extrapolate_lu_diagonal_test_2) { + DBM D(3); + D.set(0, 1, bound_t::non_strict(-2)); + D.set(0, 2, bound_t::non_strict(-2)); + D.set(1, 0, bound_t::non_strict(5)); + D.set(1, 2, bound_t::le_zero()); + D.set(2, 0, bound_t::non_strict(7)); + D.set(2, 1, bound_t::non_strict(2)); + + std::vector upper {0, 10, 10}; + std::vector lower {0, 5, 5}; + + D.extrapolate_lu_diagonal(lower, upper); + + BOOST_CHECK(D.at(0, 1) == bound_t::non_strict(-2)); + BOOST_CHECK(D.at(0, 2) == bound_t::non_strict(-2)); + BOOST_CHECK(D.at(1, 0) == bound_t::non_strict(5)); + BOOST_CHECK(D.at(1, 2) == bound_t::le_zero()); + BOOST_CHECK(D.at(2, 0) == bound_t::non_strict(7)); + BOOST_CHECK(D.at(2, 1) == bound_t::non_strict(2)); +} + BOOST_AUTO_TEST_CASE(intersection_test_1) { auto dbm1 = DBM::zero(3); auto dbm2 = DBM::zero(3);