tests/while.scop

   1 start: 83
   2 end: 210
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 schedule: '{ domain: "[n] -> { S2[x, t] : x >= 0 and x <= -1 + n and t >= 0; S1[x]
   6   : x >= 0 and x <= -1 + n; S_1[x, t] : x >= 0 and x <= -1 + n and t >= 0; R[x] :
   7   x >= 0 and x <= -1 + n }", child: { schedule: "[n] -> L_0[{ S2[x, t] -> [(x)]; S1[x]
   8   -> [(x)]; S_1[x, t] -> [(x)]; R[x] -> [(x)] }]", child: { sequence: [ { filter:
   9   "[n] -> { S1[x] }" }, { filter: "[n] -> { S2[x, t]; S_1[x, t] }", child: { schedule:
  10   "[n] -> L_1[{ S2[x, t] -> [(t)]; S_1[x, t] -> [(t)] }]", child: { sequence: [ {
  11   filter: "[n] -> { S_1[x, t] }" }, { filter: "[n] -> { S2[x, t] }" } ] } } }, { filter:
  12   "[n] -> { R[x] }" } ] } } }'
  13 arrays:
  14 - context: '{  :  }'
  15   extent: '[n] -> { __pet_test_0[x, t] : x >= 0 and x <= -1 + n and t >= 0 }'
  16   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  17   element_type: int
  18   element_size: 4
  19   uniquely_defined: 1
  20 - context: '{  :  }'
  21   extent: '[n] -> { s[] }'
  22   element_type: int
  23   element_size: 4
  24 statements:
  25 - line: 12
  26   domain: '[n] -> { S1[x] : x >= 0 and x <= -1 + n }'
  27   body:
  28     type: expression
  29     expr:
  30       type: op
  31       operation: =
  32       arguments:
  33       - type: access
  34         index: '[n] -> { S1[x] -> s[] }'
  35         reference: __pet_ref_0
  36         read: 0
  37         write: 1
  38       - type: call
  39         name: f
  40 - line: 13
  41   domain: '[n] -> { [S_1[x, t] -> [1]] : x >= 0 and x <= -1 + n and t >= 0 }'
  42   body:
  43     type: expression
  44     expr:
  45       type: op
  46       operation: =
  47       arguments:
  48       - type: access
  49         index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), (t)] }'
  50         reference: __pet_ref_2
  51         read: 0
  52         write: 1
  53       - type: call
  54         name: P
  55         arguments:
  56         - type: access
  57           index: '[n] -> { S_1[x, t] -> [(x)] }'
  58           reference: __pet_ref_3
  59           read: 1
  60           write: 0
  61         - type: access
  62           index: '[n] -> { S_1[x, t] -> s[] }'
  63           reference: __pet_ref_4
  64           read: 1
  65           write: 0
  66   arguments:
  67   - type: access
  68     index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), ((-1 + t) : t >= 1)] }'
  69     reference: __pet_ref_1
  70     read: 1
  71     write: 0
  72 - line: 14
  73   domain: '[n] -> { [S2[x, t] -> [1]] : x >= 0 and x <= -1 + n and t >= 0 }'
  74   body:
  75     type: expression
  76     expr:
  77       type: op
  78       operation: =
  79       arguments:
  80       - type: access
  81         index: '[n] -> { S2[x, t] -> s[] }'
  82         reference: __pet_ref_6
  83         read: 0
  84         write: 1
  85       - type: call
  86         name: g
  87         arguments:
  88         - type: access
  89           index: '[n] -> { S2[x, t] -> s[] }'
  90           reference: __pet_ref_7
  91           read: 1
  92           write: 0
  93   arguments:
  94   - type: access
  95     index: '[n] -> { S2[x, t] -> __pet_test_0[(x), (t)] }'
  96     reference: __pet_ref_5
  97     read: 1
  98     write: 0
  99 - line: 16
 100   domain: '[n] -> { R[x] : x >= 0 and x <= -1 + n }'
 101   body:
 102     type: expression
 103     expr:
 104       type: call
 105       name: h
 106       arguments:
 107       - type: access
 108         index: '[n] -> { R[x] -> s[] }'
 109         reference: __pet_ref_8
 110         read: 1
 111         write: 0
 112 implications:
 113 - satisfied: 1
 114   extension: '[n] -> { __pet_test_0[x, t] -> __pet_test_0[x, t''] : t'' <= t and x
 115     >= 0 and x <= -1 + n and t'' >= 0 }'