Assume relation between two symbols

Author: Petr Bauch

src/analyses/interval_domain.cpp

@@ -329,10 +329,10 @@ void interval_domaint::assume_rec(
     {
       integer_intervalt &lhs_i=int_map[lhs_identifier];
       integer_intervalt &rhs_i=int_map[rhs_identifier];
-      lhs_i.meet(rhs_i);
-      rhs_i=lhs_i;
-      if(rhs_i.is_bottom())
-        make_bottom();
+      if(id == ID_lt && !lhs_i.is_less_than(rhs_i))
+        lhs_i.make_less_than(rhs_i);
+      if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i))
+        lhs_i.make_less_than_eq(rhs_i);
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {

src/util/interval_template.h

@@ -143,6 +143,47 @@ template<class T> class interval_templatet
     }
   }
 
+  void make_bottom()
+  {
+    lower_set = upper_set = true;
+    upper = T();
+    lower = upper + 1;
+  }
+
+  void make_less_than_eq(interval_templatet &i)
+  {
+    if(upper_set && i.upper_set)
+      upper = std::min(upper, i.upper);
+    if(lower_set && i.lower_set)
+      i.lower = std::max(lower, i.lower);
+  }
+
+  void make_less_than(interval_templatet &i)
+  {
+    make_less_than_eq(i);
+    if(singleton() && i.singleton() && lower == i.lower)
+    {
+      make_bottom();
+      i.make_bottom();
+    }
+  }
+
+  bool is_less_than_eq(const interval_templatet &i)
+  {
+    if(i.lower_set && upper_set && upper <= i.lower)
+      return true;
+    else
+      return false;
+  }
+
+  bool is_less_than(const interval_templatet &i)
+  {
+    if(i.lower_set && upper_set && upper < i.lower)
+      return true;
+    else
+      return false;
+  }
+
   void approx_union_with(const interval_templatet &i)
   {
     if(i.lower_set && lower_set)