rename bound_t to extended_number everywhere except in interval files

Signed-off-by: Elazar Gershuni <[email protected]>

src/crab/array_domain.cpp

@@ -20,7 +20,7 @@
 
 namespace crab::domains {
 
-static bool maybe_between(const NumAbsDomain& dom, const bound_t& x, const linear_expression_t& symb_lb,
+static bool maybe_between(const NumAbsDomain& dom, const extended_number& x, const linear_expression_t& symb_lb,
                           const linear_expression_t& symb_ub) {
     using namespace dsl_syntax;
     assert(x.is_finite());

src/crab/ebpf_domain.cpp

@@ -3182,8 +3182,8 @@ void ebpf_domain_t::initialize_loop_counter(const label_t& label) {
     m_inv.assign(variable_t::loop_counter(to_string(label)), 0);
 }
 
-bound_t ebpf_domain_t::get_loop_count_upper_bound() const {
-    bound_t ub{0};
+extended_number ebpf_domain_t::get_loop_count_upper_bound() const {
+    extended_number ub{0};
     for (const variable_t counter : variable_t::get_loop_counters()) {
         ub = std::max(ub, m_inv[counter].ub());
     }

src/crab/ebpf_domain.hpp

@@ -49,7 +49,7 @@ class ebpf_domain_t final {
 
     typedef bool check_require_func_t(NumAbsDomain&, const linear_constraint_t&, std::string);
     void set_require_check(std::function<check_require_func_t> f);
-    bound_t get_loop_count_upper_bound() const;
+    extended_number get_loop_count_upper_bound() const;
     static ebpf_domain_t setup_entry(bool init_r1);
 
     static ebpf_domain_t from_constraints(const std::set<std::string>& constraints, bool setup_constraints);

src/crab/interval.hpp

@@ -17,6 +17,8 @@
 
 namespace crab {
 
+using bound_t = extended_number;
+
 class interval_t final {
     bound_t _lb;
     bound_t _ub;

src/crab/split_dbm.cpp

@@ -1096,8 +1096,8 @@ string_invariant SplitDBM::to_set() const {
             continue;
         }
         interval_t v_out =
-            interval_t(this->g.elem(v, 0) ? -number_t(this->g.edge_val(v, 0)) : bound_t::minus_infinity(),
-                       this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : bound_t::plus_infinity());
+            interval_t(this->g.elem(v, 0) ? -number_t(this->g.edge_val(v, 0)) : extended_number::minus_infinity(),
+                       this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : extended_number::plus_infinity());
         assert(!v_out.is_bottom());
 
         variable_t variable = *(this->rev_map[v]);
@@ -1279,8 +1279,8 @@ static interval_t get_interval(const SplitDBM::vert_map_t& m, const SplitDBM::gr
         return interval_t::top();
     }
     SplitDBM::vert_id v = it->second;
-    bound_t lb = bound_t::minus_infinity();
-    bound_t ub = bound_t::plus_infinity();
+    extended_number lb = extended_number::minus_infinity();
+    extended_number ub = extended_number::plus_infinity();
     if (r.elem(v, 0)) {
         lb = x.is_unsigned() ? (-number_t(r.edge_val(v, 0))).truncate_to_uint(finite_width)
                              : (-number_t(r.edge_val(v, 0))).truncate_to_sint(finite_width);

src/crab/thresholds.cpp

@@ -7,9 +7,9 @@ namespace crab {
 
 inline namespace iterators {
 
-void thresholds_t::add(bound_t v1) {
+void thresholds_t::add(extended_number v1) {
     if (m_thresholds.size() < m_size) {
-        bound_t v = (v1);
+        extended_number v = (v1);
         if (std::find(m_thresholds.begin(), m_thresholds.end(), v) == m_thresholds.end()) {
             auto ub = std::upper_bound(m_thresholds.begin(), m_thresholds.end(), v);
 
@@ -37,9 +37,9 @@ void thresholds_t::add(bound_t v1) {
 
 std::ostream& operator<<(std::ostream& o, const thresholds_t& t) {
     o << "{";
-    for (typename std::vector<bound_t>::const_iterator it = t.m_thresholds.begin(), et = t.m_thresholds.end();
+    for (typename std::vector<extended_number>::const_iterator it = t.m_thresholds.begin(), et = t.m_thresholds.end();
          it != et;) {
-        bound_t b(*it);
+        extended_number b(*it);
         o << b;
         ++it;
         if (it != t.m_thresholds.end()) {

src/crab/thresholds.hpp

@@ -24,22 +24,22 @@ inline namespace iterators {
 class thresholds_t final {
 
   private:
-    std::vector<bound_t> m_thresholds;
+    std::vector<extended_number> m_thresholds;
     size_t m_size;
 
   public:
     explicit thresholds_t(size_t size = UINT_MAX) : m_size(size) {
-        m_thresholds.push_back(bound_t::minus_infinity());
+        m_thresholds.push_back(extended_number::minus_infinity());
         m_thresholds.emplace_back(number_t{0});
-        m_thresholds.push_back(bound_t::plus_infinity());
+        m_thresholds.push_back(extended_number::plus_infinity());
     }
 
     [[nodiscard]]
     size_t size() const {
         return m_thresholds.size();
     }
 
-    void add(bound_t v1);
+    void add(extended_number v1);
 
     friend std::ostream& operator<<(std::ostream& o, const thresholds_t& t);
 };

src/crab_utils/num_extended.hpp

@@ -223,6 +223,4 @@ class extended_number final {
 
 }; // class extended_number
 
-using bound_t = extended_number;
-
 } // namespace crab

src/crab_verifier.cpp

@@ -31,7 +31,7 @@ struct checks_db final {
     std::map<label_t, std::vector<std::string>> m_db{};
     int total_warnings{};
     int total_unreachable{};
-    crab::bound_t max_loop_count{crab::number_t{0}};
+    crab::extended_number max_loop_count{crab::number_t{0}};
 
     void add(const label_t& label, const std::string& msg) { m_db[label].emplace_back(msg); }