tests/for_while_inc4.scop

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