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 | |
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')
-rw-r--r-- | test/regress/regress0/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/arrays/parsing_ringer.cvc | 59 | ||||
-rw-r--r-- | test/regress/regress0/bug585.cvc | 9 |
4 files changed, 73 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5e57e9b67..128783388 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -163,9 +163,10 @@ BUG_TESTS = \ bug567.smt2 \ bug576.smt2 \ bug576a.smt2 \ - bug578.smt2 + bug578.smt2 \ + bug585.cvc -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) +TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # bug512 -- taking too long, --time-per not working perhaps? in any case, # we have a minimized version still getting tested 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; diff --git a/test/regress/regress0/bug585.cvc b/test/regress/regress0/bug585.cvc new file mode 100644 index 000000000..825cb0003 --- /dev/null +++ b/test/regress/regress0/bug585.cvc @@ -0,0 +1,9 @@ +% EXPECT: sat + +Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #]; +State: TYPE = [# pc: INT, cache: Cache #]; + +s0: State; +s1: State = s0 WITH .cache[10].data := 2/3; + +CHECKSAT; |