From 5d19d98e0720ccaf993c45e2997297751a6fc1ba Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 8 Mar 2018 16:03:01 -0800 Subject: [PATCH] Fix Travis for unit test compilation errors. (#1651) make units does not fail if we have compile error for a unit test, however, make check does. -Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings. Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds. --- .travis.yml | 4 +- src/theory/theory.cpp | 5 +- test/regress/Makefile.levels | 3 + test/unit/Makefile.am | 1 + test/unit/theory/logic_info_white.h | 78 +++++++++++++------------- test/unit/theory/theory_engine_white.h | 18 +++--- 6 files changed, 56 insertions(+), 53 deletions(-) diff --git a/.travis.yml b/.travis.yml index e8c858d18..94cee00ab 100644 --- a/.travis.yml +++ b/.travis.yml @@ -81,9 +81,7 @@ script: error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED"; } makeCheck() { - make V=1 -j2 units || error "BUILD/UNIT TEST FAILED"; - make V=1 -j2 systemtests || error "BUILD/SYSTEM TEST FAILED"; - make V=1 -j2 regress0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/REGRESSION TEST FAILED"; + make V=1 -j2 check REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED" } makeExamples() { make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}"; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 2ef4f42bf..59a4d8590 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -69,8 +69,9 @@ Theory::Theory(TheoryId id, d_careGraph(NULL), d_quantEngine(NULL), d_extTheory(NULL), - d_checkTime(getStatsPrefix(id) + "::checkTime"), - d_computeCareGraphTime(getStatsPrefix(id) + "::computeCareGraphTime"), + d_checkTime(getStatsPrefix(id) + name + "::checkTime"), + d_computeCareGraphTime(getStatsPrefix(id) + name + + "::computeCareGraphTime"), d_sharedTerms(satContext), d_out(&out), d_valuation(valuation), diff --git a/test/regress/Makefile.levels b/test/regress/Makefile.levels index ecfb0c2e5..30bf4ca09 100644 --- a/test/regress/Makefile.levels +++ b/test/regress/Makefile.levels @@ -1,5 +1,8 @@ # This Makefile fragment allows one to use "make check" but also specify # a regression level. +ifeq ($(REGRESSION_LEVEL),0) +SUBDIRS = regress0 +endif ifeq ($(REGRESSION_LEVEL),1) SUBDIRS += regress1 endif diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 167100ff0..3d5f2702d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -81,6 +81,7 @@ AM_CPPFLAGS = \ $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS) AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LIBS) $(LIBS) +CXXFLAGS=-Wno-suggest-override AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 633941b2b..b70adc688 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -43,7 +43,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); @@ -60,7 +60,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); @@ -77,7 +77,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); @@ -94,7 +94,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -112,10 +112,10 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); @@ -125,10 +125,10 @@ public: info = LogicInfo("QF_AUFBV"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); @@ -138,10 +138,10 @@ public: info = LogicInfo("QF_AUFLIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); @@ -155,10 +155,10 @@ public: info = LogicInfo("QF_AX"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); @@ -168,10 +168,10 @@ public: info = LogicInfo("QF_BV"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); @@ -181,7 +181,7 @@ public: info = LogicInfo("QF_IDL"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -198,7 +198,7 @@ public: info = LogicInfo("QF_LIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -215,7 +215,7 @@ public: info = LogicInfo("QF_LRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -232,7 +232,7 @@ public: info = LogicInfo("QF_NIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -249,7 +249,7 @@ public: info = LogicInfo("QF_NRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -266,7 +266,7 @@ public: info = LogicInfo("QF_RDL"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isPure( THEORY_ARITH ) ); @@ -284,7 +284,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -297,7 +297,7 @@ public: info = LogicInfo("QF_UFBV"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -311,7 +311,7 @@ public: info = LogicInfo("QF_UFIDL"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -328,7 +328,7 @@ public: info = LogicInfo("QF_UFLIA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -345,7 +345,7 @@ public: info = LogicInfo("QF_UFLRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -361,7 +361,7 @@ public: info = LogicInfo("QF_UFNRA"); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -378,7 +378,7 @@ public: info = LogicInfo("UFLRA"); TS_ASSERT( info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -395,7 +395,7 @@ public: info = LogicInfo("UFNIA"); TS_ASSERT( info.isQuantified() ); TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isPure( THEORY_ARITH ) ); @@ -414,7 +414,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); @@ -432,7 +432,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); @@ -455,7 +455,7 @@ public: TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAYS ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); @@ -463,7 +463,7 @@ public: TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAYS ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); @@ -480,7 +480,7 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_QUANTIFIERS ) ); @@ -488,7 +488,7 @@ public: TS_ASSERT( ! info.isPure( THEORY_BOOL ) ); TS_ASSERT( ! info.isPure( THEORY_UF ) ); TS_ASSERT( ! info.isPure( THEORY_ARITH ) ); - TS_ASSERT( ! info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( ! info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( ! info.isPure( THEORY_BV ) ); TS_ASSERT( ! info.isPure( THEORY_DATATYPES ) ); TS_ASSERT( ! info.isPure( THEORY_QUANTIFIERS ) ); @@ -539,7 +539,7 @@ public: info.disableTheory(THEORY_SEP); info.lock(); TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" ); - TS_ASSERT( info.isPure( THEORY_ARRAY ) ); + TS_ASSERT( info.isPure( THEORY_ARRAYS ) ); TS_ASSERT( ! info.isQuantified() ); // check all-excluded logic @@ -551,7 +551,7 @@ public: TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); @@ -570,7 +570,7 @@ public: TS_ASSERT( !info.isSharingEnabled() ); TS_ASSERT( !info.isQuantified() ); TS_ASSERT( info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); @@ -590,7 +590,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); @@ -609,7 +609,7 @@ public: TS_ASSERT( !info.isPure( THEORY_BOOL ) ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) ); + TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index d480bbb75..e931949fd 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -206,17 +206,17 @@ public: return RewriteResponse(REWRITE_DONE, n); } - std::string identify() const throw() { + std::string identify() const override { return "Fake" + d_id; } - void presolve() { Unimplemented(); } + void presolve() override { Unimplemented(); } - void preRegisterTerm(TNode) { Unimplemented(); } + void preRegisterTerm(TNode) override { Unimplemented(); } void registerTerm(TNode) { Unimplemented(); } - void check(Theory::Effort) { Unimplemented(); } - void propagate(Theory::Effort) { Unimplemented(); } - Node explain(TNode) { Unimplemented(); } + void check(Theory::Effort) override { Unimplemented(); } + void propagate(Theory::Effort) override { Unimplemented(); } + Node explain(TNode) override { Unimplemented(); } Node getValue(TNode n) { return Node::null(); } };/* class FakeTheory */ @@ -241,7 +241,7 @@ class TheoryEngineWhite : public CxxTest::TestSuite { public: - void setUp() { + void setUp() override { d_em = new ExprManager(); d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); @@ -263,11 +263,11 @@ public: d_theoryEngine->addTheory< FakeTheory >(THEORY_BOOL); d_theoryEngine->addTheory< FakeTheory >(THEORY_UF); d_theoryEngine->addTheory< FakeTheory >(THEORY_ARITH); - d_theoryEngine->addTheory< FakeTheory >(THEORY_ARRAY); + d_theoryEngine->addTheory< FakeTheory >(THEORY_ARRAYS); d_theoryEngine->addTheory< FakeTheory >(THEORY_BV); } - void tearDown() { + void tearDown() override { delete d_nullChannel; delete d_scope; -- 2.30.2