diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
commit | 12c1e41862e4b12c3953272416a1edc103d299ee (patch) | |
tree | 9c7d3a044c33ffc3be177e6ca692eb4149add27c /test/regress | |
parent | 08df44e6b61999a14dd24a7a134146694dcb3596 (diff) |
Tuesday end-of-day commit.
Expected performance impact outside of datatypes/CVC parser is
negligible.
* CVC language LAMBDA, functional LET, type LET, precedence fixes,
bitvectors, and arrays, with partial parsing support also for
quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
these are complicated because they have to be left unresolved
at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
(not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/bv/Makefile.am | 10 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvcomp.cvc | 6 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvsimple.cvc | 41 | ||||
-rw-r--r-- | test/regress/regress0/error.cvc | 2 |
4 files changed, 47 insertions, 12 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 92db8d453..edda090ba 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -8,19 +8,19 @@ MAKEFLAGS = -k # put it below in "TESTS +=" # Regression tests for SMT inputs -SMT_TESTS = +SMT_TESTS = # Regression tests for SMT2 inputs -SMT2_TESTS = +SMT2_TESTS = # Regression tests for PL inputs CVC_TESTS = bvsimple.cvc # Regression tests derived from bug reports -BUG_TESTS = +BUG_TESTS = TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ - test00.smt - + test00.smt \ + bvcomp.smt diff --git a/test/regress/regress0/bv/bvcomp.cvc b/test/regress/regress0/bv/bvcomp.cvc new file mode 100644 index 000000000..c3397dfd7 --- /dev/null +++ b/test/regress/regress0/bv/bvcomp.cvc @@ -0,0 +1,6 @@ +% EXPECT: valid +% EXIT: 20 + +x : BITVECTOR(10); + +QUERY x /= ~x; diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc index f1cb8ff01..59fe57386 100644 --- a/test/regress/regress0/bv/bvsimple.cvc +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -4,18 +4,47 @@ % Some tests from the CVC3 user manual. % http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html +x : BITVECTOR(5); +y : BITVECTOR(4); +yy : BITVECTOR(3); + +bv : BITVECTOR(10); +a : BOOLEAN; + +xx : BITVECTOR(8); +zz : BITVECTOR(12); + +x4, y4 : BITVECTOR(4); + QUERY +( 0bin0000111101010000 = 0hex0f50 ) AND ( 0bin01@0bin0 = 0bin010 ) AND ( 0bin1000 >> 3 = 0bin0001 ) AND ( 0bin0011 << 3 = 0bin0011000 ) AND ( 0bin1000 >> 3 = 0bin0001 ) AND -TRUE - % these not working yet.. -%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND +% +%( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND %( SX(0bin100, 5) = 0bin11100 ) AND % -%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND -%( SX(0bin100, 3) = 0bin100 ) -; +%( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND +%( SX(0bin100, 3) = 0bin100 ) AND +% +%( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND +% +%( x4 = 0hex5 AND y4 = 0bin0101 ) => +%( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND +% ( NOT(BVLT(x4,y4)) ) AND +% ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND +% ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND + + +( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND +( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND + +( xx = 0hexff AND zz = 0hexff0 => + ( zz = xx << 4 ) AND + ( (zz >> 4)[7:0] = xx ) ) AND + +TRUE; diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index 982731b34..6d1641092 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,4 +1,4 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared +% EXPECT-ERROR: Parse Error: error.cvc:3.8: Symbol BOOL not declared as a type p : BOOL; % EXIT: 1 |