tests/for_while_inc.scop

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