diff options
Diffstat (limited to 'test/regress/regress0/arrays')
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/arrays/parsing_ringer.cvc | 59 |
2 files changed, 61 insertions, 1 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 345856d85..c11d68780 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -39,7 +39,8 @@ TESTS = \ incorrect11.smt \ swap_t1_np_nf_ai_00005_007.cvc.smt \ x2.smt \ - x3.smt + x3.smt \ + parsing_ringer.cvc EXTRA_DIST = $(TESTS) \ bug272.smt \ 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; |