Skip to content

Commit

Permalink
Merge pull request kind2-mc#1100 from daniel-larraz/inline-array-enum
Browse files Browse the repository at this point in the history
Honor --inline_arrays flag for arrays containing enumeration values
  • Loading branch information
daniel-larraz authored Sep 30, 2024
2 parents a0ce37b + 669f3f7 commit d73f427
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions src/lustre/lustreTransSys.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit d73f427

Please sign in to comment.