From 42c58baf0a2a96c1f3bd797d64834d02adfb9a59 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 4 Apr 2010 19:55:47 +0000 Subject: * Node::isAtomic() now looks at an "atomic" attribute of arguments instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup. --- test/regress/regress0/Makefile.am | 6 +- test/regress/regress0/boolean-prec.cvc | 3 +- test/regress/regress0/boolean.cvc | 1 + test/regress/regress0/bug1.cvc | 1 + test/regress/regress0/bug32.cvc | 1 + test/regress/regress0/error.cvc | 4 + test/regress/regress0/hole6.cvc | 1 + test/regress/regress0/logops.01.cvc | 1 + test/regress/regress0/logops.02.cvc | 1 + test/regress/regress0/logops.03.cvc | 1 + test/regress/regress0/logops.04.cvc | 1 + test/regress/regress0/logops.05.cvc | 1 + test/regress/regress0/precedence/Makefile.am | 2 +- test/regress/regress0/precedence/and-not.cvc | 1 + test/regress/regress0/precedence/and-xor.cvc | 1 + test/regress/regress0/precedence/eq-fun.cvc | 1 + test/regress/regress0/precedence/iff-assoc.cvc | 1 + test/regress/regress0/precedence/iff-implies.cvc | 1 + test/regress/regress0/precedence/implies-assoc.cvc | 1 + test/regress/regress0/precedence/implies-iff.cvc | 1 + test/regress/regress0/precedence/implies-or.cvc | 1 + test/regress/regress0/precedence/not-and.cvc | 1 + test/regress/regress0/precedence/not-eq.cvc | 1 + test/regress/regress0/precedence/or-implies.cvc | 1 + test/regress/regress0/precedence/or-xor.cvc | 1 + test/regress/regress0/precedence/xor-and.cvc | 1 + test/regress/regress0/precedence/xor-assoc.cvc | 1 + test/regress/regress0/precedence/xor-or.cvc | 1 + test/regress/regress0/queries0.cvc | 1 + test/regress/regress0/simple.cvc | 1 + test/regress/regress0/smallcnf.cvc | 1 + test/regress/regress0/test11.cvc | 1 + test/regress/regress0/test12.cvc | 1 + test/regress/regress0/test9.cvc | 1 + test/regress/regress0/uf/Makefile.am | 2 +- test/regress/regress0/uf/simple.01.cvc | 1 + test/regress/regress0/uf/simple.02.cvc | 1 + test/regress/regress0/uf/simple.03.cvc | 1 + test/regress/regress0/uf/simple.04.cvc | 1 + test/regress/regress0/uf20-03.cvc | 1 + test/regress/regress0/wiki.01.cvc | 1 + test/regress/regress0/wiki.02.cvc | 1 + test/regress/regress0/wiki.03.cvc | 1 + test/regress/regress0/wiki.04.cvc | 1 + test/regress/regress0/wiki.05.cvc | 1 + test/regress/regress0/wiki.06.cvc | 1 + test/regress/regress0/wiki.07.cvc | 1 + test/regress/regress0/wiki.08.cvc | 1 + test/regress/regress0/wiki.09.cvc | 1 + test/regress/regress0/wiki.10.cvc | 1 + test/regress/regress0/wiki.11.cvc | 1 + test/regress/regress0/wiki.12.cvc | 1 + test/regress/regress0/wiki.13.cvc | 1 + test/regress/regress0/wiki.14.cvc | 1 + test/regress/regress0/wiki.15.cvc | 1 + test/regress/regress0/wiki.16.cvc | 1 + test/regress/regress0/wiki.17.cvc | 1 + test/regress/regress0/wiki.18.cvc | 1 + test/regress/regress0/wiki.19.cvc | 1 + test/regress/regress0/wiki.20.cvc | 1 + test/regress/regress0/wiki.21.cvc | 1 + test/regress/regress1/Makefile.am | 2 +- test/regress/regress1/hole7.cvc | 1 + test/regress/regress1/hole8.cvc | 1 + test/regress/regress2/Makefile.am | 2 +- test/regress/regress2/hole9.cvc | 1 + test/regress/regress3/Makefile.am | 2 +- test/regress/regress3/hole10.cvc | 1 + test/regress/run_regression | 65 +++++-- test/unit/Makefile.am | 1 + test/unit/context/cdmap_black.h | 2 + test/unit/context/context_white.h | 186 +++++++++++++++++++++ test/unit/expr/attribute_white.h | 91 +++++++--- test/unit/expr/expr_black.h | 10 +- test/unit/expr/node_builder_black.h | 30 ++-- test/unit/theory/theory_black.h | 4 +- 76 files changed, 412 insertions(+), 60 deletions(-) create mode 100644 test/regress/regress0/error.cvc create mode 100644 test/unit/context/context_white.h (limited to 'test') diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index eb07b22fb..fe95ed7aa 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,7 +1,9 @@ SUBDIRS = precedence uf -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = \ + error.cvc \ + boolean-prec.cvc \ distinct.smt \ flet.smt \ flet2.smt \ @@ -43,7 +45,7 @@ TESTS = \ wiki.19.cvc \ wiki.20.cvc \ wiki.21.cvc - + # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc index 4f84de94d..d0205116c 100644 --- a/test/regress/regress0/boolean-prec.cvc +++ b/test/regress/regress0/boolean-prec.cvc @@ -1,6 +1,7 @@ -% Expect: VALID +% EXPECT: VALID % Simple test for right precedence of AND, <=>, NOT. A, B, C: BOOLEAN; QUERY (NOT A AND NOT B <=> C) <=> (((NOT A) AND (NOT B)) <=> C); +% EXIT: 20 diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index 89afbe325..eeac40c9f 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -804,3 +804,4 @@ a288 : BOOLEAN = ELSE FALSE ENDIF; QUERY a288; +% EXIT: 20 diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc index d3d936381..2b59638d1 100644 --- a/test/regress/regress0/bug1.cvc +++ b/test/regress/regress0/bug1.cvc @@ -6,3 +6,4 @@ ASSERT ((x > y) => f(x) > f (y)); ASSERT (x = 3); ASSERT (y = 2); QUERY(f(x) > f (y)); +% EXIT: 20 diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc index 8d113d785..c6d79a4ab 100644 --- a/test/regress/regress0/bug32.cvc +++ b/test/regress/regress0/bug32.cvc @@ -4,3 +4,4 @@ b:BOOLEAN; ASSERT(a); QUERY(a OR b); +% EXIT: 20 diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc new file mode 100644 index 000000000..09a69e212 --- /dev/null +++ b/test/regress/regress0/error.cvc @@ -0,0 +1,4 @@ +% EXPECT-ERROR: CVC4 Error: +% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared +p : BOOL; +% EXIT: 1 diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index bdd45b6d0..07bfa392c 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -177,3 +177,4 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc index d947d1a27..5348cf7e4 100644 --- a/test/regress/regress0/logops.01.cvc +++ b/test/regress/regress0/logops.01.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); +% EXIT: 20 diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc index ba2d55b4f..4a8539fae 100644 --- a/test/regress/regress0/logops.02.cvc +++ b/test/regress/regress0/logops.02.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: INVALID QUERY NOT c AND b; +% EXIT: 10 diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc index 85b23d2b0..6b5f34613 100644 --- a/test/regress/regress0/logops.03.cvc +++ b/test/regress/regress0/logops.03.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); +% EXIT: 20 diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc index a71096542..6e7aa1f5e 100644 --- a/test/regress/regress0/logops.04.cvc +++ b/test/regress/regress0/logops.04.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY (a => b) <=> (NOT a OR b); +% EXIT: 20 diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc index 19bbae5b4..14e2c887a 100644 --- a/test/regress/regress0/logops.05.cvc +++ b/test/regress/regress0/logops.05.cvc @@ -2,3 +2,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY TRUE XOR FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 0b4fcd4a6..362ec70b6 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 TESTS = \ iff-implies.cvc \ implies-iff.cvc \ diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc index d283ca881..0de37db83 100644 --- a/test/regress/regress0/precedence/and-not.cvc +++ b/test/regress/regress0/precedence/and-not.cvc @@ -4,3 +4,4 @@ A, B: BOOLEAN; QUERY (A AND NOT B) <=> (A AND (NOT B)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc index c7268727a..7b29bb95e 100644 --- a/test/regress/regress0/precedence/and-xor.cvc +++ b/test/regress/regress0/precedence/and-xor.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A AND B XOR C) <=> ((A AND B) XOR C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc index 43feeb1f8..e85b4a3e6 100644 --- a/test/regress/regress0/precedence/eq-fun.cvc +++ b/test/regress/regress0/precedence/eq-fun.cvc @@ -6,3 +6,4 @@ x , y: T; f : T -> T; QUERY (f(x) = f(y)) <=> ((f(x)) = (f(y))); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc index 82e0cbc72..b92354753 100644 --- a/test/regress/regress0/precedence/iff-assoc.cvc +++ b/test/regress/regress0/precedence/iff-assoc.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A <=> B <=> C) <=> (A <=> (B <=> C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc index bebafce14..0115fc319 100644 --- a/test/regress/regress0/precedence/iff-implies.cvc +++ b/test/regress/regress0/precedence/iff-implies.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A <=> B => C) <=> ((A <=> (B => C))); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc index c73616caf..d465df313 100644 --- a/test/regress/regress0/precedence/implies-assoc.cvc +++ b/test/regress/regress0/precedence/implies-assoc.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A => B => C) <=> (A => (B => C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc index f44c4bc75..f8c813ceb 100644 --- a/test/regress/regress0/precedence/implies-iff.cvc +++ b/test/regress/regress0/precedence/implies-iff.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A => B <=> C) <=> ((A => B) <=> C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc index 835da8570..24edb4ecd 100644 --- a/test/regress/regress0/precedence/implies-or.cvc +++ b/test/regress/regress0/precedence/implies-or.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A => B OR C) <=> (A => (B OR C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc index 44c27af53..8c849a0d9 100644 --- a/test/regress/regress0/precedence/not-and.cvc +++ b/test/regress/regress0/precedence/not-and.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (NOT A AND B) <=> ((NOT A) AND B); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc index 1126926b8..16c812086 100644 --- a/test/regress/regress0/precedence/not-eq.cvc +++ b/test/regress/regress0/precedence/not-eq.cvc @@ -4,3 +4,4 @@ A, B: BOOLEAN; QUERY (NOT A = B) <=> (NOT (A = B)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc index 3b336db5a..d91f79dc8 100644 --- a/test/regress/regress0/precedence/or-implies.cvc +++ b/test/regress/regress0/precedence/or-implies.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A OR B => C) <=> ((A OR B) => C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc index 2198962c8..47cc87c76 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A OR B XOR C) <=> (A OR (B XOR C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc index ccdaeebad..ba3f48a7f 100644 --- a/test/regress/regress0/precedence/xor-and.cvc +++ b/test/regress/regress0/precedence/xor-and.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A XOR B AND C) <=> (A XOR (B AND C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc index ffdb2c8c9..27911332c 100644 --- a/test/regress/regress0/precedence/xor-assoc.cvc +++ b/test/regress/regress0/precedence/xor-assoc.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A XOR B XOR C) <=> ((A XOR B) XOR C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc index 959dec14e..2b4436937 100644 --- a/test/regress/regress0/precedence/xor-or.cvc +++ b/test/regress/regress0/precedence/xor-or.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A XOR B OR C) <=> ((A XOR B) OR C); +% EXIT: 20 diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc index 36107e784..fe6235981 100644 --- a/test/regress/regress0/queries0.cvc +++ b/test/regress/regress0/queries0.cvc @@ -8,3 +8,4 @@ QUERY (a AND b) OR NOT (a AND b); % EXPECT: INVALID QUERY (a OR b); +% EXIT: 10 diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc index 21145b6e0..a0bff6c5a 100644 --- a/test/regress/regress0/simple.cvc +++ b/test/regress/regress0/simple.cvc @@ -5,3 +5,4 @@ ASSERT x3 OR x2; ASSERT x1 AND NOT x1; % EXPECT: VALID QUERY x2; +% EXIT: 20 diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc index 3a36b8c1e..fe17e0b53 100644 --- a/test/regress/regress0/smallcnf.cvc +++ b/test/regress/regress0/smallcnf.cvc @@ -7,3 +7,4 @@ ASSERT a OR NOT b OR c; % EXPECT: INVALID QUERY FALSE; +% EXIT: 10 diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc index 6f0cac8fa..2fa1e23ba 100644 --- a/test/regress/regress0/test11.cvc +++ b/test/regress/regress0/test11.cvc @@ -5,3 +5,4 @@ ASSERT NOT (x OR y); % EXPECT: VALID QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc index 48966f53b..a3d63b497 100644 --- a/test/regress/regress0/test12.cvc +++ b/test/regress/regress0/test12.cvc @@ -175,3 +175,4 @@ QUERY NOT P_10; POP; PUSH; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index de6be2f54..64c2011a4 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -2,3 +2,4 @@ P,Q:BOOLEAN; ASSERT (P OR Q); QUERY (P OR Q); +% EXIT: 20 diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index ec99fd45c..802189f2b 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 TESTS = \ euf_simp01.smt \ euf_simp02.smt \ diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc index f5d8c1033..84b8b8a8d 100644 --- a/test/regress/regress0/uf/simple.01.cvc +++ b/test/regress/regress0/uf/simple.01.cvc @@ -5,3 +5,4 @@ x, y: A; f: A -> B; QUERY (x = y => f(x) = f(y)); +% EXIT: 20 diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc index 0ebc319ba..21d3e3cee 100644 --- a/test/regress/regress0/uf/simple.02.cvc +++ b/test/regress/regress0/uf/simple.02.cvc @@ -5,3 +5,4 @@ x, y: A; f: A -> B; QUERY (f(x) = f(y)); +% EXIT: 10 diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc index 54948edb8..476c6cd4a 100644 --- a/test/regress/regress0/uf/simple.03.cvc +++ b/test/regress/regress0/uf/simple.03.cvc @@ -9,3 +9,4 @@ f: A -> B; ASSERT (x = a AND y = a) OR (x = b AND y = b); QUERY (f(x) = f(y)); +% EXIT: 20 diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc index 58bb6fef1..c9675588d 100644 --- a/test/regress/regress0/uf/simple.04.cvc +++ b/test/regress/regress0/uf/simple.04.cvc @@ -9,3 +9,4 @@ f: A -> B; ASSERT (x = a OR x = b) AND (y = b OR y = a); QUERY (f(x) = f(y)); +% EXIT: 10 diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc index 74fdb1116..a44b028a2 100644 --- a/test/regress/regress0/uf20-03.cvc +++ b/test/regress/regress0/uf20-03.cvc @@ -113,3 +113,4 @@ ASSERT x_10 OR NOT x_11 OR x_16; QUERY FALSE; +% EXIT: 10 diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc index 57660b5a1..7b6835469 100644 --- a/test/regress/regress0/wiki.01.cvc +++ b/test/regress/regress0/wiki.01.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR (b OR c) <=> (a OR b) OR c; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc index baba45927..9fd4f8fb7 100644 --- a/test/regress/regress0/wiki.02.cvc +++ b/test/regress/regress0/wiki.02.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND (b AND c) <=> (a AND b) AND c; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc index 791cc45c8..63c1029b4 100644 --- a/test/regress/regress0/wiki.03.cvc +++ b/test/regress/regress0/wiki.03.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR b <=> b OR a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc index f0f73ce1f..77fa0059b 100644 --- a/test/regress/regress0/wiki.04.cvc +++ b/test/regress/regress0/wiki.04.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND b <=> b AND a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index afb094dae..cb7140bcc 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR (a AND b) <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc index 421bfbdfd..6c69ca4bc 100644 --- a/test/regress/regress0/wiki.06.cvc +++ b/test/regress/regress0/wiki.06.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND (a OR b) <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc index a28cbf553..a0281d04b 100644 --- a/test/regress/regress0/wiki.07.cvc +++ b/test/regress/regress0/wiki.07.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); +% EXIT: 20 diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc index 70fc5f430..ddf0f328c 100644 --- a/test/regress/regress0/wiki.08.cvc +++ b/test/regress/regress0/wiki.08.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); +% EXIT: 20 diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc index d3118536d..f97021910 100644 --- a/test/regress/regress0/wiki.09.cvc +++ b/test/regress/regress0/wiki.09.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR NOT a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc index 41a9bcd3f..da8a1a9c3 100644 --- a/test/regress/regress0/wiki.10.cvc +++ b/test/regress/regress0/wiki.10.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND NOT a <=> FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc index e9c0b9cce..4d7c3c130 100644 --- a/test/regress/regress0/wiki.11.cvc +++ b/test/regress/regress0/wiki.11.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR a <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc index d5e7bd776..c932892c8 100644 --- a/test/regress/regress0/wiki.12.cvc +++ b/test/regress/regress0/wiki.12.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND a <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc index 2674ba47b..3ad4fd4ab 100644 --- a/test/regress/regress0/wiki.13.cvc +++ b/test/regress/regress0/wiki.13.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR FALSE <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc index 378b84dcd..454cf442c 100644 --- a/test/regress/regress0/wiki.14.cvc +++ b/test/regress/regress0/wiki.14.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND TRUE <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc index ca51c4632..81a13f798 100644 --- a/test/regress/regress0/wiki.15.cvc +++ b/test/regress/regress0/wiki.15.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR TRUE <=> TRUE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc index af47433f8..bd13faf11 100644 --- a/test/regress/regress0/wiki.16.cvc +++ b/test/regress/regress0/wiki.16.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND FALSE <=> FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc index dc7e7a1c3..48949f89f 100644 --- a/test/regress/regress0/wiki.17.cvc +++ b/test/regress/regress0/wiki.17.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT FALSE <=> TRUE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc index 21a87f4b5..8959d34a6 100644 --- a/test/regress/regress0/wiki.18.cvc +++ b/test/regress/regress0/wiki.18.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT TRUE <=> FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc index c6081c200..11366526b 100644 --- a/test/regress/regress0/wiki.19.cvc +++ b/test/regress/regress0/wiki.19.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT (a OR b) <=> NOT a AND NOT b; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc index 3bec9348b..5ef534bb0 100644 --- a/test/regress/regress0/wiki.20.cvc +++ b/test/regress/regress0/wiki.20.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT (a AND b) <=> NOT a OR NOT b; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc index e99ba2d68..bcd7146fb 100644 --- a/test/regress/regress0/wiki.21.cvc +++ b/test/regress/regress0/wiki.21.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT NOT a <=> a; +% EXIT: 20 diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 8a41e99a3..9307a33a2 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = friedman_n4_i5.smt \ hole7.cvc \ hole8.cvc \ diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc index 1bebf8049..5ff290f62 100644 --- a/test/regress/regress1/hole7.cvc +++ b/test/regress/regress1/hole7.cvc @@ -262,3 +262,4 @@ ASSERT x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51 OR x_50; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc index 65942a27f..d0f974619 100644 --- a/test/regress/regress1/hole8.cvc +++ b/test/regress/regress1/hole8.cvc @@ -371,3 +371,4 @@ ASSERT x_72 OR x_71 OR x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 2f72dd5e2..710ee6b8e 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = bmc-galileo-8.smt \ bmc-galileo-9.smt \ bmc-ibm-10.smt \ diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress2/hole9.cvc index 93377ca0b..e631444d3 100644 --- a/test/regress/regress2/hole9.cvc +++ b/test/regress/regress2/hole9.cvc @@ -507,3 +507,4 @@ ASSERT x_90 OR x_89 OR x_88 OR x_87 OR x_86 OR x_85 OR x_84 OR x_83 OR x_82; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index f0f46171c..156fffb54 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = C880mul.miter.shuffled-as.sat03-348.smt \ comb2.shuffled-as.sat03-420.smt \ hole10.cvc \ diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc index 39c978b18..661e3ef4b 100644 --- a/test/regress/regress3/hole10.cvc +++ b/test/regress/regress3/hole10.cvc @@ -673,3 +673,4 @@ ASSERT x_110 OR x_109 OR x_108 OR x_107 OR x_106 OR x_105 OR x_104 OR x_103 OR x QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/run_regression b/test/regress/run_regression index 2be776b3f..65ab6c31a 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -44,35 +44,68 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` - if [ -z "$expected_output" ]; then - error "cannot determine status of \`$benchmark'" + expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` + if [ -z "$expected_output" -a -z "$expected_error" ]; then + error "cannot determine expected output of \`$benchmark': " \ + "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" fi expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` + if [ -z "$expected_exit_status" ]; then + error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" + fi else error "benchmark \`$benchmark' must be *.cvc or *.smt" fi -expfile=`mktemp -t cvc4_expected.XXXXXXXXXX` -outfile=`mktemp -t cvc4_output.XXXXXXXXXX` -echo "$expected_output" >"$expfile" +expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX` +experrfile=`mktemp -t cvc4_expect_stderr.XXXXXXXXXX` +outfile=`mktemp -t cvc4_stdout.XXXXXXXXXX` +errfile=`mktemp -t cvc4_stderr.XXXXXXXXXX` +exitstatusfile=`mktemp -t cvc4_exitstatus.XXXXXXXXXX` +if [ -z "$expected_output" ]; then + # in case expected stdout output is empty, make sure we don't differ + # by a newline, which we would if we echo "" >"$expoutfile" + touch "$expoutfile" +else + echo "$expected_output" >"$expoutfile" +fi +if [ -z "$expected_error" ]; then + # in case expected stderr output is empty, make sure we don't differ + # by a newline, which we would if we echo "" >"$experrfile" + touch "$experrfile" +else + echo "$expected_error" >"$experrfile" +fi -# echo "$cvc4" --segv-nospin "$benchmark" -"$cvc4" --segv-nospin "$benchmark" > "$outfile" +("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile" -diffs=`diff -u "$expfile" "$outfile"` +diffs=`diff -u "$expoutfile" "$outfile"` diffexit=$? -rm -f "$expfile" +diffserr=`diff -u "$experrfile" "$errfile"` +diffexiterr=$? +exit_status=`cat "$exitstatusfile"` + +rm -f "$expoutfile" +rm -f "$experrfile" rm -f "$outfile" +rm -f "$errfile" +rm -f "$exitstatusfile" + +exitcode=0 if [ $diffexit -ne 0 ]; then - echo "$prog: error: differences between expected and actual output" + echo "$prog: error: differences between expected and actual output on stdout" echo "$diffs" - exit 1 + exitcode=1 +fi +if [ $diffexiterr -ne 0 ]; then + echo "$prog: error: differences between expected and actual output on stderr" + echo "$diffserr" + exitcode=1 fi -if [ -n "$expected_exit_status" ]; then - : - #if [ $exit_status != "$expected_exit_status" ]; then - # error "expected exit status \`$expected_exit_status' but got \`$exit_status'" - #fi +if [ "$exit_status" != "$expected_exit_status" ]; then + echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'" + exitcode=1 fi +exit $exitcode diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 768a56a9b..451100b59 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -10,6 +10,7 @@ UNIT_TESTS = \ expr/attribute_black \ parser/parser_white \ context/context_black \ + context/context_white \ context/context_mm_black \ context/cdo_black \ context/cdlist_black \ diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 7040e4cc1..262c66fe5 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -30,6 +30,8 @@ public: void setUp() { d_context = new Context; //Debug.on("cdmap"); + //Debug.on("gc"); + //Debug.on("pushpop"); } void tearDown() { diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h new file mode 100644 index 000000000..3e0928baf --- /dev/null +++ b/test/unit/context/context_white.h @@ -0,0 +1,186 @@ +/********************* */ +/** context_white.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** White box testing of CVC4::context::Context. + **/ + +#include + +#include "context/context.h" +#include "context/cdo.h" +#include "util/Assert.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class ContextWhite : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + } + + void tearDown() { + delete d_context; + } + + void testContextSimple() { + Scope *s = d_context->getTopScope(); + + TS_ASSERT(s == d_context->getBottomScope()); + TS_ASSERT(d_context->getLevel() == 0); + TS_ASSERT(d_context->d_scopeList.size() == 1); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == NULL); + + CDO a(d_context); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &a); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &s->d_pContextObjList); + + CDO b(d_context); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + + d_context->push(); + Scope* t = d_context->getTopScope(); + TS_ASSERT(s != t); + + TS_ASSERT(s == d_context->getBottomScope()); + TS_ASSERT(d_context->getLevel() == 1); + TS_ASSERT(d_context->d_scopeList.size() == 2); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &b); + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == NULL); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + + a = 5; + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &a); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &t->d_pContextObjList); + + b = 3; + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == t); + TS_ASSERT(b.d_pContextObjRestore != NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList); + + d_context->push(); + Scope* u = d_context->getTopScope(); + TS_ASSERT(u != t); + TS_ASSERT(u != s); + + CDO c(d_context); + c = 4; + + TS_ASSERT(c.d_pScope == u); + TS_ASSERT(c.d_pContextObjRestore != NULL); + TS_ASSERT(c.d_pContextObjNext == NULL); + TS_ASSERT(c.d_ppContextObjPrev == &u->d_pContextObjList); + + d_context->pop(); + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == t); + TS_ASSERT(b.d_pContextObjRestore != NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS + + d_context->pop(); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + } +}; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index fb18601a3..64c768a13 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -17,12 +17,14 @@ #include +#include "context/context.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" #include "expr/attribute.h" -#include "context/context.h" +#include "expr/node.h" +#include "theory/theory.h" +#include "theory/uf/theory_uf.h" #include "util/Assert.h" using namespace CVC4; @@ -74,24 +76,73 @@ public: } void testAttributeIds() { - TS_ASSERT(VarNameAttr::s_id == 0); - TS_ASSERT(TestStringAttr1::s_id == 1); - TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT((attr::LastAttributeId::s_id == 3)); - - TS_ASSERT(TypeAttr::s_id == 0); - TS_ASSERT((attr::LastAttributeId::s_id == 1)); - - TS_ASSERT(TestFlag1::s_id == 0); - TS_ASSERT(TestFlag2::s_id == 1); - TS_ASSERT(TestFlag3::s_id == 2); - TS_ASSERT(TestFlag4::s_id == 3); - TS_ASSERT(TestFlag5::s_id == 4); - TS_ASSERT((attr::LastAttributeId::s_id == 5)); - - TS_ASSERT(TestFlag1cd::s_id == 0); - TS_ASSERT(TestFlag2cd::s_id == 1); - TS_ASSERT((attr::LastAttributeId::s_id == 2)); + // Test that IDs for (a subset of) attributes in the system are + // unique and that the LastAttributeId (which would be the next ID + // to assign) is greater than all attribute IDs. + + // We used to check ID assignments explicitly. However, between + // compilation modules, you don't get a strong guarantee + // (initialization order is somewhat implementation-specific, and + // anyway you'd have to change the tests anytime you add an + // attribute). So we back off, and just test that they're unique + // and that the next ID to be assigned is strictly greater than + // those that have already been assigned. + + unsigned lastId = attr::LastAttributeId::s_id; + TS_ASSERT_LESS_THAN(VarNameAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestStringAttr1::s_id, lastId); + TS_ASSERT_LESS_THAN(TestStringAttr2::s_id, lastId); + + TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr1::s_id); + TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id); + TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); + + lastId = attr::LastAttributeId::s_id; + TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); + TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id); + + lastId = attr::LastAttributeId::s_id; + TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, + theory::Theory::PreRegisteredAttr::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag1::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); + + lastId = attr::LastAttributeId::s_id; + TS_ASSERT_LESS_THAN(theory::Theory::RegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); + TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag1cd::s_id); + TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id); + TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); + + lastId = attr::LastAttributeId::s_id; + TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId); } void testCDAttributes() { diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h index e253b4a24..03d4ba31c 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_black.h @@ -354,7 +354,9 @@ public: TS_ASSERT(mult->isAtomic()); TS_ASSERT(plus->isAtomic()); TS_ASSERT(d->isAtomic()); - TS_ASSERT(!null->isAtomic()); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException); +#endif /* CVC4_ASSERTIONS */ TS_ASSERT(i1->isAtomic()); TS_ASSERT(i2->isAtomic()); @@ -368,6 +370,12 @@ public: TS_ASSERT(!x.isAtomic()); TS_ASSERT(!y.isAtomic()); TS_ASSERT(!z.isAtomic()); + + Expr w1 = d_em->mkExpr(PLUS, d_em->mkExpr(ITE, z, *i1, *i2), *i2); + Expr w2 = d_em->mkExpr(PLUS, d_em->mkExpr(MULT, *i1, *i2), *i2); + + TS_ASSERT(!w1.isAtomic()); + TS_ASSERT(w2.isAtomic()); } void testGetConst() { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 81aa424f8..2a7b3623e 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -244,9 +244,9 @@ public: Node n = noKind; -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(noKind.getKind(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); @@ -277,11 +277,11 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS noKind << specKind; n = noKind; - TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() ); -#endif + TS_ASSERT_THROWS( noKind.getNumChildren(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } void testOperatorSquare() { @@ -297,10 +297,10 @@ public: Node i_2 = d_nm->mkConst(true); Node i_K = d_nm->mkNode(NOT, i_0); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(arr[-1];); - TS_ASSERT_THROWS_ANYTHING(arr[0];); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(arr[-1], AssertionException); + TS_ASSERT_THROWS(arr[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ arr << i_0; @@ -330,10 +330,10 @@ public: } TS_ASSERT_EQUALS(arr[K], i_K); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS Node n = arr; - TS_ASSERT_THROWS_ANYTHING(arr[0]); -#endif + TS_ASSERT_THROWS(arr[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testClear() { @@ -469,6 +469,10 @@ public: Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z); Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException); +#endif /* CVC4_ASSERTIONS */ + NodeBuilder<> b; // test append(TNode) diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 427a22c9d..c6da48291 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -82,13 +82,13 @@ public: } }; -class DummyTheory : public TheoryImpl { +class DummyTheory : public Theory { public: set d_registered; vector d_getSequence; DummyTheory(Context* ctxt, OutputChannel& out) : - TheoryImpl(ctxt, out) { + Theory(ctxt, out) { } void registerTerm(TNode n) { -- cgit v1.2.3