Compressed bounds

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()));

src/pardibaal/bound_t.cpp

@@ -21,79 +21,72 @@
  */
 
 #include <ostream>
+#include <cassert>
 
 #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();
 
-        return bound_t(this->get_bound() + rhs.get_bound(), this->is_strict() || rhs.is_strict());
+        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((((val1 >> 1) + (val2 >> 1)) << 1) | strictness);
     }
 
     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");
+
+        const val_t lhs = this->_data;
+        const val_t strictness = 1 & lhs;
 
-    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((((lhs >> 1) + rhs) << 1) | strictness);
     }
 
-    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;
+
+        assert(get_bound() > BOUND_VAL_MIN + rhs && rhs > BOUND_VAL_MIN && rhs < BOUND_VAL_MAX && "Underflow");
 
-        if (this->get_bound() == rhs.get_bound())
-            return !rhs.is_strict() && this->is_strict();
+        const val_t lhs = this->_data;
+        const val_t strictness = 1 & lhs;
 
-        return this->get_bound() < rhs.get_bound();
+        return bound_t((((lhs >> 1) - rhs) << 1) | strictness);
     }
 
-    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;
+
+        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"));
+
+        const val_t lhs = this->_data;
+        const val_t strictness = 1 & lhs;
 
-        return (this->get_bound() == rhs.get_bound()) && (this->is_strict() == rhs.is_strict());
+        return bound_t((((lhs >> 1) * rhs) << 1) | strictness);
     }
 
-    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;}

src/pardibaal/bound_t.h

@@ -25,46 +25,58 @@
 
 #include <ostream>
 #include <cinttypes>
+#include <limits>
 
 
 namespace pardibaal {
     using dim_t = uint32_t;
     using val_t = int32_t;
 
-    enum strict_e {STRICT, NON_STRICT};
+    /**
+     * 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<int32_t>::max();
+    const int32_t LE_ZERO_BOUND = 1;
+    const int32_t LT_ZERO_BOUND = 0;
+    const int32_t BOUND_VAL_MAX = std::numeric_limits<int32_t>::max() >> 1;
+    const int32_t BOUND_VAL_MIN = std::numeric_limits<int32_t>::min() >> 1;
+
+    enum strict_e {STRICT = 0, NON_STRICT = 1};
 
     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) {
+            _data = (n << 1) | (val_t) strictness;
+        }
+
+        constexpr bound_t(val_t n, bool strict) {
+            _data = (n << 1) | (val_t) !strict;
+        }
+
+        [[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 +85,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;

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());
             }

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);
-}
+}

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());
 }