tests/for_while_inc4.scop

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