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); S1[x1] : x1 >= 0 and x1 <= -1
   7   + n; S_1[x1, x2] : exists (e0 = floor((-1 + x2)/2): 2e0 = -1 + x2 and x1 >= 0 and
   8   x1 <= -1 + n and x2 >= 9); R[x1] : x1 >= 0 and x1 <= -1 + n }", child: { schedule:
   9   "[n] -> L_0[{ S1[x1] -> [(x1)]; R[x1] -> [(x1)]; S_1[x1, x2] -> [(x1)]; S2[x1, x2]
  10   -> [(x1)] }]", child: { sequence: [ { filter: "[n] -> { S1[x1] }" }, { filter: "[n]
  11   -> { S2[x1, x2]; S_1[x1, x2] }", child: { schedule: "[n] -> L_1[{ S_1[x1, x2] ->
  12   [(x2)]; S2[x1, x2] -> [(x2)] }]", child: { sequence: [ { filter: "[n] -> { S_1[x1,
  13   x2] }" }, { filter: "[n] -> { S2[x1, x2] }" } ] } } }, { filter: "[n] -> { R[x1]
  14   }" } ] } } }'
  15 arrays:
  16 - context: '{  :  }'
  17   extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = floor((-1 + x2)/2): 2e0 =
  18     -1 + x2 and x1 <= -1 + n and x2 >= 9 and x1 >= 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 statements:
  28 - line: 12
  29   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  30   body:
  31     type: expression
  32     expr:
  33       type: op
  34       operation: =
  35       arguments:
  36       - type: access
  37         index: '[n] -> { S1[x1] -> s[] }'
  38         reference: __pet_ref_0
  39         read: 0
  40         write: 1
  41       - type: call
  42         name: f
  43 - line: 13
  44   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = floor((-1 + x2)/2): 2e0 =
  45     -1 + x2 and x1 <= -1 + n and x2 >= 9 and x1 >= 0) }'
  46   body:
  47     type: expression
  48     expr:
  49       type: op
  50       operation: =
  51       arguments:
  52       - type: access
  53         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  54         reference: __pet_ref_2
  55         read: 0
  56         write: 1
  57       - type: call
  58         name: P
  59         arguments:
  60         - type: access
  61           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  62           reference: __pet_ref_3
  63           read: 1
  64           write: 0
  65         - type: access
  66           index: '[n] -> { S_1[x1, x2] -> [(x2)] }'
  67           reference: __pet_ref_4
  68           read: 1
  69           write: 0
  70   arguments:
  71   - type: access
  72     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((-2 + x2) : x2 >= 11)] }'
  73     reference: __pet_ref_1
  74     read: 1
  75     write: 0
  76 - line: 14
  77   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = floor((-1 + x2)/2): 2e0 = -1
  78     + x2 and x1 <= -1 + n and x2 >= 9 and x1 >= 0) }'
  79   body:
  80     type: expression
  81     expr:
  82       type: op
  83       operation: =
  84       arguments:
  85       - type: access
  86         index: '[n] -> { S2[x1, x2] -> s[] }'
  87         reference: __pet_ref_6
  88         read: 0
  89         write: 1
  90       - type: call
  91         name: g
  92         arguments:
  93         - type: access
  94           index: '[n] -> { S2[x1, x2] -> s[] }'
  95           reference: __pet_ref_7
  96           read: 1
  97           write: 0
  98   arguments:
  99   - type: access
 100     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
 101     reference: __pet_ref_5
 102     read: 1
 103     write: 0
 104 - line: 16
 105   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
 106   body:
 107     type: expression
 108     expr:
 109       type: call
 110       name: h
 111       arguments:
 112       - type: access
 113         index: '[n] -> { R[x1] -> s[] }'
 114         reference: __pet_ref_8
 115         read: 1
 116         write: 0
 117 implications:
 118 - satisfied: 1
 119   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 120     = floor((-1 + x2'')/2): 2e0 = -1 + x2'' and x2'' <= x2 and x1 >= 0 and x1 <= -1
 121     + n and x2'' >= 9) }'