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         relation: '[n] -> { S1[x1] -> s[] }'
  32         index: '[n] -> { S1[x1] -> s[] }'
  33         reference: __pet_ref_0
  34         read: 0
  35         write: 1
  36       - type: call
  37         name: f
  38 - line: 14
  39   domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }'
  40   schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 0] }'
  41   body:
  42     type: expression
  43     expr:
  44       type: op
  45       operation: =
  46       arguments:
  47       - type: access
  48         relation: '[n] -> { S_1[x1] -> x2[] }'
  49         index: '[n] -> { S_1[x1] -> x2[] }'
  50         reference: __pet_ref_1
  51         read: 0
  52         write: 1
  53       - type: int
  54         value: 0
  55 - line: 14
  56   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
  57   schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 1, t, 0] }'
  58   body:
  59     type: expression
  60     expr:
  61       type: op
  62       operation: =
  63       arguments:
  64       - type: access
  65         relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }'
  66         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  67         reference: __pet_ref_3
  68         read: 0
  69         write: 1
  70       - type: call
  71         name: P
  72         arguments:
  73         - type: access
  74           relation: '[n] -> { S_2[x1, t] -> [x1] }'
  75           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
  76           reference: __pet_ref_4
  77           read: 1
  78           write: 0
  79         - type: access
  80           relation: '[n] -> { S_2[x1, t] -> x2[] }'
  81           index: '[n] -> { S_2[x1, t] -> x2[] }'
  82           reference: __pet_ref_5
  83           read: 1
  84           write: 0
  85   arguments:
  86   - type: access
  87     relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }'
  88     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
  89     reference: __pet_ref_2
  90     read: 1
  91     write: 0
  92 - line: 15
  93   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
  94   schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 1, t, 1, 0] }'
  95   body:
  96     type: expression
  97     expr:
  98       type: op
  99       operation: =
 100       arguments:
 101       - type: access
 102         relation: '[n] -> { S2[x1, t] -> s[] }'
 103         index: '[n] -> { S2[x1, t] -> s[] }'
 104         reference: __pet_ref_7
 105         read: 0
 106         write: 1
 107       - type: call
 108         name: g
 109         arguments:
 110         - type: access
 111           relation: '[n] -> { S2[x1, t] -> s[] }'
 112           index: '[n] -> { S2[x1, t] -> s[] }'
 113           reference: __pet_ref_8
 114           read: 1
 115           write: 0
 116   arguments:
 117   - type: access
 118     relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }'
 119     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 120     reference: __pet_ref_6
 121     read: 1
 122     write: 0
 123 - line: 14
 124   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 125   schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 1, t, 2] }'
 126   body:
 127     type: expression
 128     expr:
 129       type: op
 130       operation: +=
 131       arguments:
 132       - type: access
 133         relation: '[n] -> { S_4[x1, t] -> x2[] }'
 134         index: '[n] -> { S_4[x1, t] -> x2[] }'
 135         reference: __pet_ref_10
 136         read: 0
 137         write: 1
 138       - type: access
 139         relation: '[n] -> { S_4[x1, t] -> [n] }'
 140         index: '[n] -> { S_4[x1, t] -> [(n)] }'
 141         reference: __pet_ref_11
 142         read: 1
 143         write: 0
 144   arguments:
 145   - type: access
 146     relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }'
 147     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 148     reference: __pet_ref_9
 149     read: 1
 150     write: 0
 151 - line: 17
 152   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 153   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 154   body:
 155     type: expression
 156     expr:
 157       type: call
 158       name: h
 159       arguments:
 160       - type: access
 161         relation: '[n] -> { R[x1] -> s[] }'
 162         index: '[n] -> { R[x1] -> s[] }'
 163         reference: __pet_ref_12
 164         read: 1
 165         write: 0
 166 implications:
 167 - satisfied: 1
 168   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 169     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'