add support for using forall index in linear constraint

src/lib/Templates.ml

@@ -84,7 +84,15 @@ let instantiate_convex_predicate (param_map : var_map) (inv : convex_predicate)
 
 let rec instantiate_linear_term (param_map : var_map) (term : unexpanded_linear_term) : unexpanded_linear_term =
   match term with
-    | Unexpanded_constant _ | Unexpanded_variable (_, Var_name _) -> term
+    | Unexpanded_constant _ -> term
+    | Unexpanded_variable (c, Var_name name) -> begin
+        match Hashtbl.find_opt param_map name with
+          | None ->  Unexpanded_variable (c, Var_name name)
+          | Some (Arg_name name') -> Unexpanded_variable (c, Var_name name')
+          | Some (Arg_int i_val) -> Unexpanded_constant i_val
+          | Some (Arg_float f_val) -> Unexpanded_constant f_val
+          | Some (Arg_bool _) -> failwith "[instantiate_linear_term]: boolean variable in linear constraint."
+    end
     | Unexpanded_variable (c, Var_array_access (arr_name, index)) ->
         let index' = instantiate_discrete_arithmetic_expression param_map index in
         Unexpanded_variable (c, Var_array_access (arr_name, index'))

tests/testcases/templates/syntatic_check.imi

@@ -13,7 +13,7 @@ template p(i : int)
 
 actions: acts[2 * i];
 
-loc A: invariant x[i] <= params[2 * i]
+loc A: invariant x[i] <= params[i]
   when id = IDLE do { x[i] := 0 } sync acts[2 * i] goto req;
 
 loc req: invariant x[i] <= k
@@ -28,17 +28,18 @@ loc cs: invariant True
 
 end
 
-forall i in [0, 2]: instantiate p[i] := p(i);
+forall i in [0, 1]: instantiate p[i] := p(i);
 
 init := {
 
     discrete =
+        forall i in [0, 1]: loc[p[i]] := A,
         id := IDLE,
     ;
 
     continuous =
-        x[0] = 0
-      & x[1] = 0
+        forall i in [0, 1]: x[i] = i &
+        forall i in [0, 1]: params[i] >= 0
     ;
 }