TP3: Réduction d'un état

Pystan/config/sign_analysis.py

@@ -344,11 +344,33 @@ def reduce_strict_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
     if res is None: return None
     return s | { x: res }
 
-def reduce_state(s: state,c: BoolExpr) -> state:
-    if s is None: return s
+def reduce_state(s: state, c: BoolExpr) -> state:
+    if s is None:
+        return s
+
     match c:
-        # To be completed (see course's slides)
-        case _: return s
+        case BEEq(AEVar(x), expr):
+            return reduce_eq_sign(s, x, expr)
+        case BEEq(expr, AEVar(x)):
+            return reduce_eq_sign(s, x, expr)
+
+        case BELeq(AEVar(x), expr):
+            return reduce_upper_bound(s, x, expr)
+        case BELeq(expr, AEVar(x)):
+            return reduce_lower_bound(s, x, expr)
+
+        case BENeg(BEEq(AEVar(x), expr)):
+            return reduce_neq_sign(s, x, expr)
+        case BENeg(BEEq(expr, AEVar(x))):
+            return reduce_neq_sign(s, x, expr)
+
+        case BENeg(BELeq(AEVar(x), expr)):
+            return reduce_strict_lower_bound(s, x, expr)
+        case BENeg(BELeq(expr, AEVar(x))):
+            return reduce_strict_upper_bound(s, x, expr)
+
+        case _:
+            return s
 
 class Sign_interp(Transfer[state]):
     variables: frozenset[str]