diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-08 17:36:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-08 17:36:50 +0000 |
commit | c0dcc5ff59473a45864f818cfdda037c0ee4ea12 (patch) | |
tree | fba897c7bea5f5a12b65c0818b7c5260f48e0070 /test | |
parent | 8b01efc32d61391d8d3cd2aaac0de49cd8e88ecc (diff) |
Bugs resolved by this commit: #314, #322, #359, #364, #365.
See below for details.
* Fix the "assert" name-collision bug (resolves bug #364).
Our identifiers should never be named "assert", as that's a preprocessor
definition in <assert.h>, which is often #included indirectly (so simply
having a policy of not including <assert.h> isn't good enough---one of
our dependences might include it). It was once the case that we didn't
have anything named "assert", but "assert()" has now crept back in.
Instead, name things "assertFoo()" or similar. Thanks to Tim for the
report.
To fix this, I've changed some of Dejan's circuit-propagator code from
"assert()" to "assertTrue()". Ditto for Andy's explanation manager.
Guys, if you prefer a different name in your code, please change it.
* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
Inner lets now shadow outer lets (previously, they incorrectly gave an
error). Additionally, while looking at this, I found that a sequential let
was implemented rather than a parallel let. This is now fixed. Thanks to
Liana for the report.
* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).
* There were a lot of Debug lines in bitvectors that had embedded toString()
calls. This wasted a LOT of time in debug builds for BV benchmarks
(like in "make regress"). Added if(Debug.isOn(...)) guards; much faster
now.
* Support for building public-facing interface documentation only (as opposed
to all internals documentation). Now "make doc" does the public-facing and
"make doc-internals" does documentation of everything. (Along with changes
to the nightly build script---which will now build and publish both types
of Doxygen documentation---this resolves bug #359).
* Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the
report (a long long time ago--sorry).
* The default output language for all streams is now based on the current set
of Options (if there is one). This has been a constant annoyance, especially
when stringstreams are used to construct output. However, it doesn't work
for calls from outside the library, so it's mainly an annoyance-fixer for
CVC4 library code itself.
* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
are used only in assertions-enabled builds (and thus give warnings in
production builds). This was briefly discussed at the meeting this week.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 8 | ||||
-rw-r--r-- | test/regress/regress0/bug322.cvc | 23 | ||||
-rw-r--r-- | test/regress/regress0/bug322b.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/bug365.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/rec2.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress0/parallel-let.smt2 | 9 |
6 files changed, 60 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5eda230c3..58788c194 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -43,7 +43,8 @@ SMT2_TESTS = \ simple-lra.smt2 \ simple-rdl.smt2 \ simple-uf.smt2 \ - simplification_bug4.smt2 + simplification_bug4.smt2 \ + parallel-let.smt2 # Regression tests for PL inputs CVC_TESTS = \ @@ -115,7 +116,10 @@ BUG_TESTS = \ buggy-ite.smt2 \ bug303.smt2 \ bug310.cvc \ - bug339.smt2 + bug322.cvc \ + bug322b.cvc \ + bug339.smt2 \ + bug365.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug322.cvc b/test/regress/regress0/bug322.cvc new file mode 100644 index 000000000..c68fde795 --- /dev/null +++ b/test/regress/regress0/bug322.cvc @@ -0,0 +1,23 @@ +% EXPECT: sat +% EXIT: 10 +% Preamble -------------- +DATATYPE UNIT = Unit END; +DATATYPE BOOL = Truth | Falsity END; + +% Decls -------------- +node$type: TYPE; +value$type: TYPE; +Nodes$elem$type: TYPE = node$type; +Nodes$t$type: TYPE; +node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL; +failure_pattern$type: TYPE = node_pair_set$type; +is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, + deliver: failure_pattern$type): + (IF (EXISTS (q: node$type): + (NOT ((((deliver)[ + (p)])[ + (q)]) = + (Truth)))) THEN + (Truth) ELSE (Falsity) ENDIF)); + +CHECKSAT; diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc new file mode 100644 index 000000000..d10292dd5 --- /dev/null +++ b/test/regress/regress0/bug322b.cvc @@ -0,0 +1,12 @@ +% COMMAND-LINE: --incremental +% EXPECT: valid +% EXPECT: valid +% EXPECT: valid +% EXIT: 20 +x : INT; +y : INT = x + 1; +z : INT = -10; +identity : INT -> INT = LAMBDA(x:INT) : x; +QUERY identity(x) = x; +QUERY identity(y) > x; +QUERY identity(z) = -10; diff --git a/test/regress/regress0/bug365.smt2 b/test/regress/regress0/bug365.smt2 new file mode 100644 index 000000000..6dd48a849 --- /dev/null +++ b/test/regress/regress0/bug365.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LIA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(assert (let + ((a 2)) + (= a (let ((a 7)) a)))) +(check-sat) +(exit) + diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc index 80aecfe25..49684241c 100644 --- a/test/regress/regress0/datatypes/rec2.cvc +++ b/test/regress/regress0/datatypes/rec2.cvc @@ -1,7 +1,7 @@ % EXPECT: valid % EXIT: 20 c : BOOLEAN; -a16 : [# _a : REAL, _b : REAL #] = ( +a16 : [# _a : INT, _b : INT #] = ( IF c THEN (# _a := 3, _b := 2 #) ELSE (# _a := 1, _b := 5 #) ENDIF WITH ._a := 2); diff --git a/test/regress/regress0/parallel-let.smt2 b/test/regress/regress0/parallel-let.smt2 new file mode 100644 index 000000000..1f12522ee --- /dev/null +++ b/test/regress/regress0/parallel-let.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(assert (distinct x y)) +(assert (let ((x y) (y x)) (= x y))) +(check-sat) +(exit) |