diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-03-25 05:32:31 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-03-25 05:32:31 +0000 |
commit | a2472774f053ed0ab98f1508ebb313466b0fe29a (patch) | |
tree | 2241c713acff99b23b1b51cb33c8a7a63c5afac4 /test/regress | |
parent | ee36b95b8f722fe6501cc6ac635efd49ca673791 (diff) |
This is a merge from the "theoryfixes+cdattrhash" branch. The changes
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/Makefile.am | 6 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/arith/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/Makefile.am | 12 | ||||
-rw-r--r-- | test/regress/regress0/lemmas/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/precedence/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 8 | ||||
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress1/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress1/arith/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress2/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress3/Makefile.am | 2 |
13 files changed, 24 insertions, 24 deletions
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 3867ee860..37f474cfc 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -12,13 +12,13 @@ regress3: regress0 regress1 regress2 regress0 regress1 regress2 regress3: -cd $@ && $(MAKE) check -# synonyms for "check" +# synonyms for "checK" in this directory in this directory .PHONY: regress test regress test: check # no-ops here -.PHONY: units -units: +.PHONY: units systemtests +units systemtests: EXTRA_DIST = \ run_regression \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 37020d48e..dbc493678 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -84,7 +84,6 @@ BUG_TESTS = \ bug167.smt \ bug168.smt \ bug187.smt2 \ - bug216.smt2 \ bug220.smt2 \ bug239.smt \ buggy-ite.smt2 @@ -92,6 +91,7 @@ BUG_TESTS = \ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ + bug216.smt2 \ bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION @@ -104,7 +104,7 @@ endif EXTRA_DIST += \ error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index aca076d9f..83078c177 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -23,7 +23,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index e204a29b5..19d458403 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -41,7 +41,7 @@ TESTS = \ equality-00.smt \ equality-01.smt \ equality-02.smt \ - equality-05.smt \ + equality-05.smt \ bv_eq_diamond10.smt \ slice-01.smt \ slice-02.smt \ @@ -67,13 +67,13 @@ TESTS = \ a78test0002.smt \ a95test0002.smt \ bitvec0.smt \ - bitvec2.smt \ + bitvec2.smt + +EXTRA_DIST = $(TESTS) \ bitvec3.smt \ - bitvec5.smt - -EXTRA_DIST = $(TESTS) + bitvec5.smt -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index bc99f81af..65a009aa2 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -21,7 +21,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 88defc40b..36de2ceb3 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -35,7 +35,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index ee365e79d..223f2f9ee 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -9,14 +9,14 @@ MAKEFLAGS = -k # Regression tests for SMT inputs CVC_TESTS = \ - test.00.cvc \ - test.01.cvc + test.00.cvc TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + test.01.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 2e05386e0..06f45bca2 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -41,7 +41,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 3ebd95257..2f81b04eb 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -27,7 +27,7 @@ BUG_TESTS = TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 10fe5f01a..d58debe82 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -26,7 +26,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress1 test regress regress1 test: check diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am index 4bdff93d1..e23579fc7 100644 --- a/test/regress/regress1/arith/Makefile.am +++ b/test/regress/regress1/arith/Makefile.am @@ -12,7 +12,7 @@ TESTS = \ EXTRA_DIST = $(TESTS) -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress1 test regress regress1 test: check diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 28a814274..77d9ef158 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -36,7 +36,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress2 test regress regress2 test: check diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index fca3c4ef8..ada9664d3 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -25,7 +25,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress3 test regress regress3 test: check |