tests/for_while_inc4.scop

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