tests/inc5.scop

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