tests/assume5.scop

   1 start: 23
   2 end: 100
   3 indent: "\t"
   4 context: '{  :  }'
   5 schedule: '{ domain: "{ S_0[]; S_2[]; S_1[] }", child: { sequence: [ { filter: "{
   6   S_0[] }" }, { filter: "{ S_1[] }" }, { filter: "{ S_2[] }" } ] } }'
   7 arrays:
   8 - context: '{  :  }'
   9   extent: '{ a[] }'
  10   element_type: int
  11   element_size: 4
  12 - context: '{  :  }'
  13   extent: '{ k[] }'
  14   element_type: int
  15   element_size: 4
  16 statements:
  17 - line: 5
  18   domain: '{ S_0[] }'
  19   body:
  20     type: expression
  21     expr:
  22       type: op
  23       operation: assume
  24       arguments:
  25       - type: op
  26         operation: '>='
  27         arguments:
  28         - type: access
  29           index: '{ S_0[] -> k[] }'
  30           reference: __pet_ref_0
  31           read: 1
  32           write: 0
  33         - type: int
  34           value: 0
  35 - line: 6
  36   domain: '{ S_1[] }'
  37   body:
  38     type: expression
  39     expr:
  40       type: op
  41       operation: =
  42       arguments:
  43       - type: access
  44         index: '{ S_1[] -> k[] }'
  45         reference: __pet_ref_1
  46         read: 0
  47         write: 1
  48       - type: op
  49         operation: '-'
  50         arguments:
  51         - type: int
  52           value: 1
  53 - line: 7
  54   domain: '{ S_2[] }'
  55   body:
  56     type: expression
  57     expr:
  58       type: op
  59       operation: =
  60       arguments:
  61       - type: access
  62         index: '{ S_2[] -> a[] }'
  63         reference: __pet_ref_2
  64         read: 0
  65         write: 1
  66       - type: access
  67         index: '{ S_2[] -> [(-1)] }'
  68         reference: __pet_ref_3
  69         read: 1
  70         write: 0