TP3: Treillis des intervalles, début

Pystan/config/interval_analysis.py

@@ -141,7 +141,16 @@ def interval_opp(i: Interval) -> Interval:
     return Interval(l,u)
 
 def interval_add(i1: Interval, i2: Interval) -> Interval:
-    raise NotImplementedError
+    if i1.lower_bound is None or i2.lower_bound is None:
+        l = None
+    else:
+        l = i1.lower_bound + i2.lower_bound
+    if i1.upper_bound is None or i2.upper_bound is None:
+        u = None
+    else:
+        u = i1.upper_bound + i2.upper_bound
+    return Interval(l, u)
+
 
 def interval_mul_pos(i1: Interval, i2: Interval) -> Interval:
     assert (i1.lower_bound is not None and i1.lower_bound >= 0)
@@ -180,7 +189,20 @@ def interval_mul(i1: Interval, i2: Interval) -> Interval:
     return res
 
 def interval_div(i1: Interval, i2: Interval) -> Interval | Top | None:
-    raise NotImplementedError
+    if is_zero(i2):
+        return None
+    if contains_zero(i2):
+        return Top()
+    # i2 ne contient pas 0 : pas d'erreur
+    bounds = []
+    for a in [i1.lower_bound, i1.upper_bound]:
+        for b in [i2.lower_bound, i2.upper_bound]:
+            if a is not None and b is not None:
+                bounds.append(a // b)
+    if not bounds:
+        return Interval(None, None)
+    return Interval(min(bounds), max(bounds))
+
 
 def eval_aexp(env: abstract_env, e: ArithExpr) -> Interval | Top | None:
     """evaluate an arithmetic expression in an abstract environment
@@ -261,17 +283,44 @@ def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
             return not v
         case _: pass
 
-def reduce_eq(s:state, x:str, i: Interval) -> state:
-    raise NotImplementedError
-
-def reduce_neq(s:state, x: str, i: Interval) -> state:
-    raise NotImplementedError
-
-def reduce_leq(s:state,x:str,upper_bound: int) -> state:
-    raise NotImplementedError
+def reduce_eq(s: state, x: str, i: Interval) -> state:
+    if s is None: return None
+    res = interval_meet(s[x], i)
+    if res is None: return None
+    s1 = s.copy()
+    s1[x] = res
+    return s1
+
+def reduce_neq(s: state, x: str, i: Interval) -> state:
+    if s is None: return None
+    cur = s[x]
+    if i.lower_bound == i.upper_bound == cur.lower_bound == cur.upper_bound:
+        return None
+    # if it's a singleton and inside the current interval
+    if i.lower_bound == i.upper_bound:
+        l, u = cur.lower_bound, cur.upper_bound
+        if l is not None and u is not None:
+            if i.lower_bound == l and i.upper_bound < u:
+                return s | {x: Interval(i.lower_bound + 1, u)}
+            elif i.upper_bound == u and i.lower_bound > l:
+                return s | {x: Interval(l, i.upper_bound - 1)}
+    return s
+
+def reduce_leq(s: state, x: str, upper_bound: int) -> state:
+    if s is None: return None
+    cur = s[x]
+    new_upper = min(cur.upper_bound, upper_bound) if cur.upper_bound is not None else upper_bound
+    if cur.lower_bound is not None and cur.lower_bound > new_upper:
+        return None
+    return s | {x: Interval(cur.lower_bound, new_upper)}
 
 def reduce_geq(s: state, x: str, lower_bound: int) -> state:
-    raise NotImplementedError
+    if s is None: return None
+    cur = s[x]
+    new_lower = max(cur.lower_bound, lower_bound) if cur.lower_bound is not None else lower_bound
+    if cur.upper_bound is not None and cur.upper_bound < new_lower:
+        return None
+    return s | {x: Interval(new_lower, cur.upper_bound)}
 
 def reduce_state(s: state,c: BoolExpr) -> state:
     if s is None: return s