test/regress/regress0/arrays/parsing_ringer.cvc

   1 % Test for presentiation language parsing, some edge cases with cascading
   2 % store terms.  Intended to put this part of the parser "through the ringer,"
   3 % hence the name.
   4
   5 % COMMAND-LINE: --incremental
   6 % EXPECT: sat
   7 % EXPECT: sat
   8 % EXPECT: sat
   9 % EXPECT: sat
  10 % EXPECT: sat
  11 % EXPECT: sat
  12
  13 PUSH;
  14
  15 x, y : ARRAY INT OF ARRAY INT OF ARRAY INT OF INT;
  16
  17 % multidimensional arrays
  18 ASSERT x[0][0][0] = 0; %% select
  19 ASSERT y = x WITH [0][0][1] := 1; %% partial store
  20
  21 CHECKSAT;
  22
  23 % mixed stores: records of arrays of tuples, oh my
  24 z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #];
  25
  26 arr1 : ARRAY INT OF [# x:INT #];
  27 arr2 : [ ARRAY INT OF INT, ARRAY INT OF INT ];
  28
  29 ASSERT arr1[0].x = 0;
  30 ASSERT arr2.0[0] = 1;
  31 ASSERT arr2.1[0] = 5;
  32
  33 ASSERT z.y.1[1] /= 1;
  34 ASSERT (# x:=arr1, y:=arr2 #) = z;
  35
  36 CHECKSAT;
  37
  38 ASSERT z.x[0].x /= z.y.0[5];
  39
  40 CHECKSAT;
  41
  42 ASSERT z.y.0[1] = z.x[5].x;
  43
  44 CHECKSAT;
  45
  46 ASSERT z.y.0[5] = z.x[-2].x;
  47
  48 CHECKSAT;
  49
  50 POP;
  51
  52 a : ARRAY INT OF ARRAY INT OF INT;
  53 b : ARRAY INT OF INT;
  54
  55 % ambiguity in presentation language, comma needs to bind to innermost WITH
  56 % causes type error if the [2]:=2 at the end is attached to the wrong WITH
  57 ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2;
  58
  59 CHECKSAT;