diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 18:05:31 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 14:26:53 -0400 |
commit | 627628cd06fc5b19fe59c95b3cb4073d85a8dfab (patch) | |
tree | a9fc919209fceea59257a18c7142015d0043d763 /test/regress/regress0/arrays/parsing_ringer.cvc | |
parent | 65f0dc22fe49c6c388e9413f3b7541d7fb49a3b3 (diff) |
Fix native language parsing of chained-store expressions (resolves bug 585). Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.
Diffstat (limited to 'test/regress/regress0/arrays/parsing_ringer.cvc')
-rw-r--r-- | test/regress/regress0/arrays/parsing_ringer.cvc | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc new file mode 100644 index 000000000..c9f8c9e22 --- /dev/null +++ b/test/regress/regress0/arrays/parsing_ringer.cvc @@ -0,0 +1,59 @@ +% Test for presentiation language parsing, some edge cases with cascading +% store terms. Intended to put this part of the parser "through the ringer," +% hence the name. + +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat + +PUSH; + +x, y : ARRAY INT OF ARRAY INT OF ARRAY INT OF INT; + +% multidimensional arrays +ASSERT x[0][0][0] = 0; %% select +ASSERT y = x WITH [0][0][1] := 1; %% partial store + +CHECKSAT; + +% mixed stores: records of arrays of tuples, oh my +z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #]; + +arr1 : ARRAY INT OF [# x:INT #]; +arr2 : [ ARRAY INT OF INT, ARRAY INT OF INT ]; + +ASSERT arr1[0].x = 0; +ASSERT arr2.0[0] = 1; +ASSERT arr2.1[0] = 5; + +ASSERT z.y.1[1] /= 1; +ASSERT (# x:=arr1, y:=arr2 #) = z; + +CHECKSAT; + +ASSERT z.x[0].x /= z.y.0[5]; + +CHECKSAT; + +ASSERT z.y.0[1] = z.x[5].x; + +CHECKSAT; + +ASSERT z.y.0[5] = z.x[-2].x; + +CHECKSAT; + +POP; + +a : ARRAY INT OF ARRAY INT OF INT; +b : ARRAY INT OF INT; + +% ambiguity in presentation language, comma needs to bind to innermost WITH +% causes type error if the [2]:=2 at the end is attached to the wrong WITH +ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2; + +CHECKSAT; |