tests/for_while_inc.scop

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