diff options
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()); } |