Merge pull request kind2-mc#1032 from daniel-larraz/qvar-enum-subrange

Handle quantified enum/subrange variables

src/lustre/lustreAstHelpers.ml

@@ -109,6 +109,17 @@ let rec type_contains_subrange = function
   | ArrayType (_, (ty, _)) -> type_contains_subrange ty
   | _ -> false
 
+let rec type_contains_enum_or_subrange = function
+  | IntRange _
+  | EnumType _ -> true
+  | TupleType (_, tys) | GroupType (_, tys) ->
+    List.fold_left (fun acc ty -> acc || type_contains_enum_or_subrange ty) false tys
+  | RecordType (_, _, tys) ->
+    List.fold_left (fun acc (_, _, ty) -> acc || type_contains_enum_or_subrange ty)
+      false tys
+  | ArrayType (_, (ty, _)) -> type_contains_enum_or_subrange ty
+  | _ -> false
+
 (* Substitute t for var. AnyOp and Quantifier are not supported due to introduction of bound variables. *)
 let rec substitute_naive (var:HString.t) t = function
   | Ident (_, i) as e -> if i = var then t else e

src/lustre/lustreAstHelpers.mli

@@ -48,6 +48,9 @@ val type_arity : lustre_type -> int * int
 val type_contains_subrange : lustre_type -> bool
 (** Returns true if the lustre type expression contains an IntRange or if it is an IntRange *)
 
+val type_contains_enum_or_subrange : lustre_type -> bool
+(** Returns true if the lustre type expression contains an EnumType/IntRange or if it is an EnumType/IntRange *)
+
 val type_contains_array : lustre_type -> bool 
 (** Returns true if the lustre type expression contains an array or if it is an array *)
 

src/lustre/lustreAstNormalizer.ml

@@ -397,6 +397,19 @@ let mk_range_expr ctx expr_type expr =
   let rec mk ctx n expr_type expr = 
     let expr_type = Ctx.expand_nested_type_syn ctx expr_type in
     match expr_type with
+    | A.EnumType (_, _, values) -> (
+      let eqs =
+        List.map (fun v -> A.CompOp (dpos, A.Eq, expr, A.Ident(dpos, v) )) values
+      in
+      match eqs with
+      | [] -> assert false
+      | [e] -> [e, true]
+      | e :: eqs ->
+        let disj =
+          List.fold_left (fun acc e' -> A.BinaryOp(dpos, A.Or, acc, e')) e eqs
+        in
+        [disj, true]
+    )
     | A.IntRange (_, l, u) ->
       let original_ty = Chk.infer_type_expr ctx expr |> unwrap in
       let original_ty = Ctx.expand_nested_type_syn ctx original_ty in
@@ -1213,7 +1226,34 @@ and normalize_expr ?guard info map =
       in
       let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ty nexpr in
       iexpr, union gids1 gids2, warnings
-  in function
+  in let mk_enum_subrange_constraints info vars =
+    let enum_subrange_vars =
+      vars |> List.filter (fun (_, _, ty) ->
+        let ty = Ctx.expand_nested_type_syn info.context ty in
+        AH.type_contains_enum_or_subrange ty
+      )
+    in
+    let constraints =
+      List.fold_left
+        (fun acc (_, id, ty) ->
+          let expr = A.Ident(dpos, id) in
+          let range_exprs = mk_range_expr info.context ty expr in
+          range_exprs :: acc
+        )
+        []
+        enum_subrange_vars
+      |> List.flatten |> List.map fst
+    in
+    match constraints with
+    | [] -> None
+    | c :: cs ->
+      let conj =
+        List.fold_left
+          (fun acc c' -> A.BinaryOp (dpos, A.And, c', acc)) c cs
+      in
+      Some conj
+  in
+  function
   (* ************************************************************************ *)
   (* Node calls                                                               *)
   (* ************************************************************************ *)
@@ -1423,6 +1463,15 @@ and normalize_expr ?guard info map =
         quantified_variables = info.quantified_variables @ vars }
     in
     let nexpr, gids, warnings = normalize_expr ?guard info map expr in
+    let nexpr =
+      let constraints =
+        mk_enum_subrange_constraints info vars
+      in
+      match constraints, kind with
+      | None, _ -> nexpr
+      | Some c, A.Exists -> A.BinaryOp (pos, A.And, c, nexpr)
+      | Some c, A.Forall -> A.BinaryOp (pos, A.Impl, c, nexpr)
+    in
     Quantifier (pos, kind, vars, nexpr), gids, warnings
   | When (pos, expr, clock_expr) ->
     let nexpr, gids, warnings = normalize_expr ?guard info map expr in

tests/regression/success/quantified_subrange_var.lus

@@ -0,0 +1,12 @@
+
+type T = subrange [0,1] of int;
+
+type E = enum {E1, E2};
+
+node N() returns (ok: bool);
+let
+  check forall (x: T) x<5;
+  check exists (x:T) 0<x;
+  check forall (x: E) x=E1 or x=E2;
+  check exists (x: E) x=E1;
+tel