removed computing of guard_bdu in views_domain, because it is already…

… computed in the global information
Kappa-Dev · Jan 29, 2025 · 561595c · 561595c
1 parent 959839e
commit 561595c
Show file tree

Hide file tree

Showing 4 changed files with 146 additions and 154 deletions.
diff --git a/core/KaSa_rep/reachability_analysis/analyzer_headers.ml b/core/KaSa_rep/reachability_analysis/analyzer_headers.ml
@@ -268,6 +268,9 @@ let set_guard_mvbdus guard_mvbdus static =
 let set_restriction_mvbdu restriction_mvbdu static =
   { static with global_restriction_mvbdu = restriction_mvbdu }
 
+let get_guard_mvbdus static = static.global_guard_mvbdus
+let get_restriction_mvbdu static = static.global_restriction_mvbdu
+
 (*****************************************************************************)
 (*RULE*)
 (*****************************************************************************)

diff --git a/core/KaSa_rep/reachability_analysis/analyzer_headers.mli b/core/KaSa_rep/reachability_analysis/analyzer_headers.mli
@@ -218,6 +218,13 @@ val compute_initial_state :
 val get_kappa_handler : global_static_information -> Cckappa_sig.kappa_handler
 val get_cc_code : global_static_information -> Cckappa_sig.compil
 
+val get_guard_mvbdus :
+  global_static_information ->
+  Ckappa_sig.Views_bdu.mvbdu Ckappa_sig.Rule_setmap.Map.t
+
+val get_restriction_mvbdu :
+  global_static_information -> Ckappa_sig.Views_bdu.mvbdu
+
 val get_mvbdu_handler :
   global_dynamic_information -> Mvbdu_wrapper.Mvbdu.handler