From 1ba5430f27d3f617f36cb45d3ba11f77c792f0ba Mon Sep 17 00:00:00 2001
From: Yassine Ettayeb <yassine.ettayeb@student-cs.fr>
Date: Fri, 28 Mar 2025 09:44:20 +0100
Subject: [PATCH] =?UTF-8?q?TP3:=20R=C3=A9duction=20d'un=20=C3=A9tat?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
Pystan/config/sign_analysis.py | 30 ++++++++++++++++++++++++++----
1 file changed, 26 insertions(+), 4 deletions(-)
diff --git a/Pystan/config/sign_analysis.py b/Pystan/config/sign_analysis.py
index 043f5b1..38b4e9e 100644
--- a/Pystan/config/sign_analysis.py
+++ b/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]
--
GitLab