Merge pull request #1100 from daniel-larraz/inline-array-enum

Honor --inline_arrays flag for arrays containing enumeration values
kind2-mc · Sep 30, 2024 · d73f427 · d73f427
2 parents a0ce37b + 669f3f7
commit d73f427
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml
@@ -460,6 +460,13 @@ let add_constraints_of_type init terms state_var =
       List.fold_left
         (fun acc (ty, iv) ->
            match Type.node_of_type ty with
+           | Type.IntRange (Some i, Some j) when Flags.Arrays.inline () -> (
+              let cj = ref [] in
+              for x = (Numeral.to_int j) downto (Numeral.to_int i) do
+                cj := Term.mk_let [iv, Term.mk_num_of_int x] acc :: !cj
+              done;
+              Term.mk_and !cj
+           )
            | Type.IntRange (Some i, Some j) -> (
              let bounds =
                Term.mk_leq