tests/loop7.scop

   1 start: 40
   2 end: 114
   3 indent: "\t"
   4 context: '{  :  }'
   5 schedule: '{ domain: "{ S_3[t] : t >= 0; S_0[]; S_2[t] : t >= 0; S_4[t] : t >= 0;
   6   S_1[] }", child: { sequence: [ { filter: "{ S_0[] }" }, { filter: "{ S_1[] }" },
   7   { filter: "{ S_3[t]; S_2[t]; S_4[t] }", child: { schedule: "L_0[{ S_2[t] -> [(t)];
   8   S_3[t] -> [(t)]; S_4[t] -> [(t)] }]", child: { sequence: [ { filter: "{ S_2[t] }"
   9   }, { filter: "{ S_3[t] }" }, { filter: "{ S_4[t] }" } ] } } } ] } }'
  10 arrays:
  11 - context: '{  :  }'
  12   extent: '{ __pet_test_0[t] : t >= 0 }'
  13   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  14   element_type: int
  15   element_size: 4
  16   uniquely_defined: 1
  17 - context: '{  :  }'
  18   extent: '{ a[] }'
  19   element_type: int
  20   element_size: 4
  21 - context: '{  :  }'
  22   extent: '{ i[] }'
  23   element_type: int
  24   element_size: 4
  25 statements:
  26 - line: 9
  27   domain: '{ S_0[] }'
  28   body:
  29     type: expression
  30     expr:
  31       type: op
  32       operation: =
  33       arguments:
  34       - type: access
  35         index: '{ S_0[] -> i[] }'
  36         reference: __pet_ref_0
  37         read: 0
  38         write: 1
  39       - type: call
  40         name: f
  41 - line: 10
  42   domain: '{ S_1[] }'
  43   body:
  44     type: expression
  45     expr:
  46       type: op
  47       operation: =
  48       arguments:
  49       - type: access
  50         index: '{ S_1[] -> i[] }'
  51         reference: __pet_ref_1
  52         read: 0
  53         write: 1
  54       - type: access
  55         index: '{ S_1[] -> i[] }'
  56         reference: __pet_ref_2
  57         read: 1
  58         write: 0
  59 - line: 10
  60   domain: '{ [S_2[t] -> [1]] : t >= 0 }'
  61   body:
  62     type: expression
  63     expr:
  64       type: op
  65       operation: =
  66       arguments:
  67       - type: access
  68         index: '{ S_2[t] -> __pet_test_0[(t)] }'
  69         reference: __pet_ref_4
  70         read: 0
  71         write: 1
  72       - type: op
  73         operation: <
  74         arguments:
  75         - type: access
  76           index: '{ S_2[t] -> i[] }'
  77           reference: __pet_ref_5
  78           read: 1
  79           write: 0
  80         - type: int
  81           value: 10
  82   arguments:
  83   - type: access
  84     index: '{ S_2[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  85     reference: __pet_ref_3
  86     read: 1
  87     write: 0
  88 - line: 11
  89   domain: '{ [S_3[t] -> [1]] : t >= 0 }'
  90   body:
  91     type: expression
  92     expr:
  93       type: op
  94       operation: =
  95       arguments:
  96       - type: access
  97         index: '{ S_3[t] -> a[] }'
  98         reference: __pet_ref_7
  99         read: 0
 100         write: 1
 101       - type: int
 102         value: 5
 103   arguments:
 104   - type: access
 105     index: '{ S_3[t] -> __pet_test_0[(t)] }'
 106     reference: __pet_ref_6
 107     read: 1
 108     write: 0
 109 - line: 10
 110   domain: '{ [S_4[t] -> [1]] : t >= 0 }'
 111   body:
 112     type: expression
 113     expr:
 114       type: op
 115       operation: +=
 116       arguments:
 117       - type: access
 118         index: '{ S_4[t] -> i[] }'
 119         reference: __pet_ref_9
 120         read: 0
 121         write: 1
 122       - type: int
 123         value: 1
 124   arguments:
 125   - type: access
 126     index: '{ S_4[t] -> __pet_test_0[(t)] }'
 127     reference: __pet_ref_8
 128     read: 1
 129     write: 0
 130 implications:
 131 - satisfied: 1
 132   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'