Merge branch 'main' into compressed_bounds

DEIS-Tools · Sep 14, 2023 · 9c6827a · 9c6827a
2 parents 6f2e627 + 1c8f7c2
commit 9c6827a
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 42 deletions.
diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp
@@ -50,14 +50,6 @@ namespace pardibaal {
         return dbm;
     }
 
-    // bound_t DBM::at(dim_t i, dim_t j) const {return this->_bounds_table.at(i, j);}
-
-    // void DBM::set(dim_t i, dim_t j, bound_t bound) {this->_bounds_table.set(i, j, bound);}
-
-    // void DBM::set(const difference_bound_t& constraint) {
-    //     this->_bounds_table.set(constraint._i, constraint._j, constraint._bound);
-    // }
-
     void DBM::subtract(dim_t i, dim_t j, bound_t bound) {
         if (this->at(i, j) > bound) // if i,j,bound is larger than current, then result is empty. Always false if bound is inf
             this->restrict(j, i, bound_t(-bound.get_bound(), bound.is_non_strict()));
@@ -234,19 +226,11 @@ namespace pardibaal {
             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)));
+                                                              _bounds_table.at(i, k) + _bounds_table.at(k, j)));
 
         _is_closed = true;
     }
 
-    void DBM::close_single_bound(dim_t i, dim_t j) {
-        const dim_t dim = this->dimension();
-
-        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() {
         const dim_t dim = this->dimension();
 

diff --git a/src/pardibaal/DBM.h b/src/pardibaal/DBM.h
@@ -68,17 +68,14 @@ namespace pardibaal {
         mutable empty_status_e _empty_status = NON_EMPTY;
         mutable bool _is_closed = true;
 
-        // Set bound (i, j) to the shortest/lowest (canonical) form
-        void close_single_bound(dim_t i, dim_t j);
-
     public:
         DBM(dim_t number_of_clocks);
 
         static DBM zero(dim_t dimension);
 
         static DBM unconstrained(dim_t dimension);
 
-        [[nodiscard]] inline bound_t at(dim_t i, dim_t j) const {return this->_bounds_table.at(i, j);}
+        [[nodiscard]] inline bound_t at(dim_t i, dim_t j) const { return this->_bounds_table.at(i, j); }
 
         inline void set(dim_t i, dim_t j, bound_t bound) {
             this->_bounds_table.set(i, j, bound);
@@ -90,6 +87,8 @@ namespace pardibaal {
             this->set(constraint._i, constraint._j, constraint._bound);
         }
 
+        [[nodiscard]] inline empty_status_e empty_status() const { return _empty_status; }
+
         void subtract(dim_t i, dim_t j, bound_t bound);
         void subtract(difference_bound_t constraint);
 

diff --git a/src/pardibaal/bounds_table_t.cpp b/src/pardibaal/bounds_table_t.cpp
@@ -35,25 +35,6 @@ namespace pardibaal {
 
     dim_t bounds_table_t::number_of_clocks() const {return this->_number_of_clocks;}
 
-//     bound_t bounds_table_t::at(dim_t i, dim_t j) const {
-// #ifndef NEXCEPTIONS
-//         if (i >= _number_of_clocks || j >= _number_of_clocks)
-//             throw base_error("ERROR: Out of bounds access on coordinate: ", i, ", ", j, " with dimensions: ",
-//                              _number_of_clocks);
-// #endif
-
-//         return _bounds[i * _number_of_clocks + j];
-//     }
-
-//     void bounds_table_t::set(dim_t i, dim_t j, bound_t bound) {
-// #ifndef NEXCEPTIONS
-//         if (i >= _number_of_clocks || j >= _number_of_clocks)
-//             throw base_error("ERROR: Out of bounds access on coordinate: ", i, ", ", j, " with dimensions: ",
-//                              _number_of_clocks);
-// #endif
-//         this->_bounds[i * _number_of_clocks + j] = bound;
-//     }
-
     std::ostream& operator<<(std::ostream& out, const bounds_table_t& table) {
         out << '\n';
         for (dim_t i = 0; i < table._number_of_clocks; ++i) {

diff --git a/src/pardibaal/bounds_table_t.h b/src/pardibaal/bounds_table_t.h
@@ -40,8 +40,13 @@ namespace pardibaal {
          */
         [[nodiscard]] dim_t number_of_clocks() const;
 
-        [[nodiscard]] inline bound_t at(dim_t i, dim_t j) const {return _bounds[i * _number_of_clocks + j];}
-        inline void set(dim_t i, dim_t j, bound_t bound) {this->_bounds[i * _number_of_clocks + j] = bound;};
+        [[nodiscard]] inline bound_t at(dim_t i, dim_t j) const {
+            return _bounds[i * _number_of_clocks + j];
+        }
+
+        inline void set(dim_t i, dim_t j, bound_t bound) { 
+            this->_bounds[i * _number_of_clocks + j] = bound; 
+        }
 
         friend std::ostream& operator<<(std::ostream& out, const bounds_table_t& table);