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 | |
| 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')
23 files changed, 263 insertions, 96 deletions
diff --git a/test/Makefile.am b/test/Makefile.am index e370752b6..98e1c8b86 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -2,15 +2,15 @@ SUBDIRS = unit system regress . MAKEFLAGS = -k -.PHONY: units regress regress0 regress1 regress2 regress3 -units regress regress0 regress1 regress2 regress3: +.PHONY: units systemtests regress regress0 regress1 regress2 regress3 +units systemtests regress regress0 regress1 regress2 regress3: @$(MAKE) check-pre; \ for dir in $(SUBDIRS); do \ test $$dir = . || (cd $$dir && $(MAKE) $(AM_MAKEFLAGS) $@); \ done; \ $(MAKE) check-local -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: test test: check @@ -37,6 +37,9 @@ check-local: if test -s "unit/test-suite.log"; then :; else \ echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \ fi; \ + if test -s "system/test-suite.log"; then :; else \ + echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \ + fi; \ for dir in $(subdirs_to_check); do \ log=$$dir/test-suite.log; \ if test -s "$$log"; then \ 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 diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 954798e6c..7e0192340 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -1,5 +1,7 @@ TESTS_ENVIRONMENT = -TESTS = +TESTS = \ + boilerplate \ + ouroborous # Things that aren't tests but that tests rely on and need to # go into the distribution @@ -28,20 +30,43 @@ else system_LINK = $(CXXLINK) endif +AM_CPPFLAGS = \ + -I. \ + "-I@top_srcdir@/src/include" \ + "-I@top_srcdir@/lib" \ + "-I@top_srcdir@/src" \ + "-I@top_builddir@/src" \ + "-I@top_srcdir@/src/prop/minisat" \ + -D __STDC_LIMIT_MACROS \ + -D __STDC_FORMAT_MACROS \ + $(TEST_CPPFLAGS) +LIBADD = \ + @abs_top_builddir@/src/parser/libcvc4parser.la \ + @abs_top_builddir@/src/libcvc4.la + # WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS: -# system_test: system_test.cpp -# $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@.lo $< -# $(AM_V_CXXLD)$(system_LINK) $(AM_LDFLAGS) $@.lo +$(TESTS:%=%.lo): %.lo: %.cpp + $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+ +$(TESTS): %: %.lo $(LIBADD) + $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $< + +# trick automake into setting LTCXXCOMPILE, CXXLINK, etc. +if CVC4_FALSE +noinst_LTLIBRARIES = libdummy.la +nodist_libdummy_la_SOURCES = ouroborous.cpp +libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la +endif # rebuild tests if a library changes -$(TESTS):: $(TEST_DEPS) +#$(TESTS):: $(TEST_DEPS) +MAKEFLAGS = -k export VERBOSE = 1 -# synonyms for "check" -.PHONY: test -test: check +# synonyms for "checK" in this directory in this directory +.PHONY: test systemtests +test systemtests: check # no-ops here -.PHONY: units regress regress0 regress1 regress2 regress3s +.PHONY: units regress regress0 regress1 regress2 regress3 units regress regress0 regress1 regress2 regress3: diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp new file mode 100644 index 000000000..89d5174e3 --- /dev/null +++ b/test/system/boilerplate.cpp @@ -0,0 +1,38 @@ +/********************* */ +/*! \file boilerplate.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief A simple start-up/tear-down test for CVC4. + ** + ** This simple test just makes sure that the public interface is + ** minimally functional. It is useful as a template to use for other + ** system tests. + **/ + +#include <iostream> +#include <sstream> + +#include "expr/expr.h" +#include "smt/smt_engine.h" + +using namespace CVC4; +using namespace std; + +int main() { + ExprManager em; + Options opts; + SmtEngine smt(&em, opts); + Result r = smt.query(em.mkConst(true)); + + return r == Result::VALID ? 0 : 1; +} + diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp new file mode 100644 index 000000000..4473b42bb --- /dev/null +++ b/test/system/ouroborous.cpp @@ -0,0 +1,103 @@ +/********************* */ +/*! \file ouroborous.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief "Ouroborous" test: does CVC4 read its own output? + ** + ** The "Ouroborous" test, named after the serpent that swallows its own + ** tail, ensures that CVC4 can parse some input, output it again (in any + ** of its languages) and then parse it again. The result of the first + ** parse must be equal to the result of the second parse (up to renaming + ** variables), or the test fails. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::language; +using namespace std; + +const string declarations = "\ +(declare-sort U 0)\n\ +(declare-fun f (U) U)\n\ +(declare-fun x () U)\n\ +(declare-fun y () U)\n\ +(assert (= (f x) x))\n\ +"; + +int runTest(); + +int main() { + try { + return runTest(); + } catch(Exception& e) { + cerr << e << endl; + } catch(...) { + cerr << "non-cvc4 exception thrown." << endl; + } + return 1; +} + +string translate(Parser* parser, string in, InputLanguage inlang, OutputLanguage outlang) { + cout << "==============================================" << endl + << "translating from " << inlang << " to " << outlang << " this string:" << endl + << in << endl; + parser->setInput(Input::newStringInput(inlang, in, "internal-buffer")); + stringstream ss; + ss << Expr::setlanguage(outlang) << parser->nextExpression(); + AlwaysAssert(parser->nextExpression().isNull(), "next expr should be null"); + AlwaysAssert(parser->done(), "parser should be done"); + string s = ss.str(); + cout << "got this:" << endl + << s << endl + << "==============================================" << endl; + return s; +} + +int runTest() { + ExprManager em; + Parser* parser = + ParserBuilder(em, "internal-buffer") + .withStringInput(declarations) + .withInputLanguage(input::LANG_SMTLIB_V2) + .build(); + + // we don't need to execute them, but we DO need to parse them to + // get the declarations + while(Command* c = parser->nextCommand()) { + delete c; + } + + AlwaysAssert(parser->done(), "parser should be done"); + + string instr = "(= (f (f y)) x)"; + string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2); + string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB); + //string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4); + //string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); + string out = smt1; + + AlwaysAssert(out == smt2, "differences in output"); + + delete parser; + + return 0; +} + diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 725d4a4bb..eb70935e7 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -172,7 +172,7 @@ nodist_libdummy_la_SOURCES = expr/node_black.cpp libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la endif -# synonyms for "check" +# synonyms for "checK" in this directory in this directory .PHONY: units test units test: check diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index a121029f3..3dbee87eb 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -26,6 +26,7 @@ #include "expr/node_manager.h" #include "expr/attribute.h" #include "expr/node.h" +#include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "util/Assert.h" @@ -108,17 +109,11 @@ public: //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); lastId = attr::LastAttributeId<bool, false>::s_id; - 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(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); @@ -131,12 +126,15 @@ public: TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); lastId = attr::LastAttributeId<bool, true>::s_id; -// TS_ASSERT_LESS_THAN(TheoryEngine::RegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::Asserted::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); -// TS_ASSERT_DIFFERS(TheoryEngine::RegisteredAttr::s_id, TestFlag1cd::s_id); -// TS_ASSERT_DIFFERS(TheoryEngine::RegisteredAttr::s_id, TestFlag2cd::s_id); + TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag1cd::s_id); + TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag2cd::s_id); TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); + cout << "A: " << theory::Asserted::s_id << endl; + cout << "1: " << TestFlag1cd::s_id << endl; + cout << "2: " << TestFlag2cd::s_id << endl; lastId = attr::LastAttributeId<Node, false>::s_id; // TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId); @@ -156,27 +154,27 @@ public: } void testCDAttributes() { - //Debug.on("boolattr"); + //Debug.on("cdboolattr"); Node a = d_nm->mkVar(*d_booleanType); Node b = d_nm->mkVar(*d_booleanType); Node c = d_nm->mkVar(*d_booleanType); - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->push(); // level 1 // test that all boolean flags are FALSE to start - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); // test that they all HAVE the boolean attributes @@ -186,96 +184,96 @@ public: // test two-arg version of hasAttribute() bool bb = false; - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(a.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(b.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(c.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); // setting boolean flags - Debug("boolattr", "set flag 1 on a to T\n"); + Debug("cdboolattr", "set flag 1 on a to T\n"); a.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "set flag 1 on b to F\n"); + Debug("cdboolattr", "set flag 1 on b to F\n"); b.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on c to F\n"); + Debug("cdboolattr", "set flag 1 on c to F\n"); c.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "get flag 1 on a (should be T)\n"); + Debug("cdbootattr", "get flag 1 on a (should be T)\n"); TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdbootattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->push(); // level 2 - Debug("boolattr", "get flag 1 on a (should be T)\n"); + Debug("cdbootattr", "get flag 1 on a (should be T)\n"); TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdbootattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); - Debug("boolattr", "set flag 1 on a to F\n"); + Debug("cdbootattr", "set flag 1 on a to F\n"); a.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on b to T\n"); + Debug("cdbootattr", "set flag 1 on b to T\n"); b.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); + Debug("cdbootattr", "get flag 1 on b (should be T)\n"); TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->push(); // level 3 - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); + Debug("cdbootattr", "get flag 1 on b (should be T)\n"); TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); - Debug("boolattr", "set flag 1 on c to T\n"); + Debug("cdbootattr", "set flag 1 on c to T\n"); c.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); + Debug("cdbootattr", "get flag 1 on b (should be T)\n"); TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be T)\n"); + Debug("cdbootattr", "get flag 1 on c (should be T)\n"); TS_ASSERT(c.getAttribute(TestFlag1cd())); d_ctxt->pop(); // level 2 - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); + Debug("cdbootattr", "get flag 1 on b (should be T)\n"); TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->pop(); // level 1 - Debug("boolattr", "get flag 1 on a (should be T)\n"); + Debug("cdbootattr", "get flag 1 on a (should be T)\n"); TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdbootattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->pop(); // level 0 - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdbootattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); #ifdef CVC4_ASSERTIONS @@ -284,7 +282,7 @@ public: } void testAttributes() { - //Debug.on("boolattr"); + //Debug.on("bootattr"); Node a = d_nm->mkVar(*d_booleanType); Node b = d_nm->mkVar(*d_booleanType); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 4aee8060f..9de8f94b4 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -96,7 +96,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_arith = new TheoryArith(d_ctxt, d_outputChannel); + d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL)); preregistered = new std::set<Node>(); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 18408acd3..a362a597c 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -104,8 +104,8 @@ public: set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(Context* ctxt, OutputChannel& out) : - Theory(theory::THEORY_BUILTIN, ctxt, out) { + DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) : + Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) { } void registerTerm(TNode n) { @@ -142,7 +142,7 @@ public: void preRegisterTerm(TNode n) {} void propagate(Effort level) {} void explain(TNode n, Effort level) {} - Node getValue(TNode n, Valuation* valuation) { return Node::null(); } + Node getValue(TNode n) { return Node::null(); } string identify() const { return "DummyTheory"; } }; @@ -165,7 +165,7 @@ public: d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_dummy = new DummyTheory(d_ctxt, d_outputChannel); + d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL)); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 5915ac1f7..f99698204 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -107,8 +107,8 @@ class FakeTheory : public Theory { // static std::deque<RewriteItem> s_expected; public: - FakeTheory(context::Context* ctxt, OutputChannel& out) : - Theory(theoryId, ctxt, out) + FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) : + Theory(theoryId, ctxt, out, valuation) { } /** Register an expected rewrite call */ @@ -212,7 +212,7 @@ public: void check(Theory::Effort) { Unimplemented(); } void propagate(Theory::Effort) { Unimplemented(); } void explain(TNode, Theory::Effort) { Unimplemented(); } - Node getValue(TNode n, Valuation* valuation) { return Node::null(); } + Node getValue(TNode n) { return Node::null(); } };/* class FakeTheory */ diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h index 19b289ae7..1940bc199 100644 --- a/test/unit/theory/theory_uf_tim_white.h +++ b/test/unit/theory/theory_uf_tim_white.h @@ -61,7 +61,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_euf = new TheoryUFTim(d_ctxt, d_outputChannel); + d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL)); d_booleanType = new TypeNode(d_nm->booleanType()); } |