From 11a34205808098e503f145b2a779078dd509729e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 23 Aug 2018 16:28:21 -0700 Subject: [PATCH] Add missing overrides in unit tests (#2362) --- test/unit/base/map_util_black.h | 4 +- test/unit/context/cdlist_black.h | 4 +- test/unit/context/cdmap_black.h | 5 ++- test/unit/context/cdmap_white.h | 14 +++---- test/unit/context/cdo_black.h | 14 +++---- test/unit/context/context_black.h | 33 ++++++---------- test/unit/context/context_mm_black.h | 14 +++---- test/unit/context/context_white.h | 16 +++----- test/unit/expr/attribute_black.h | 9 +++-- test/unit/expr/attribute_white.h | 9 +++-- test/unit/expr/expr_manager_public.h | 20 +++++----- test/unit/expr/expr_public.h | 24 +++++++----- test/unit/expr/kind_black.h | 10 +++-- test/unit/expr/node_black.h | 6 ++- test/unit/expr/node_builder_black.h | 9 +++-- test/unit/expr/node_manager_black.h | 9 +++-- test/unit/expr/node_manager_white.h | 9 +++-- test/unit/expr/node_self_iterator_black.h | 9 +++-- test/unit/expr/node_white.h | 9 +++-- test/unit/expr/symbol_table_black.h | 16 +++++--- test/unit/expr/type_cardinality_public.h | 28 +++++++------- test/unit/expr/type_node_white.h | 9 +++-- test/unit/main/interactive_shell_black.h | 5 ++- test/unit/parser/parser_black.h | 27 ++++--------- test/unit/parser/parser_builder_black.h | 4 +- test/unit/preprocessing/pass_bv_gauss_white.h | 4 +- test/unit/prop/cnf_stream_white.h | 38 +++++++++++-------- test/unit/theory/evaluator_white.h | 4 +- test/unit/theory/theory_arith_white.h | 6 ++- test/unit/theory/theory_black.h | 9 +++-- test/unit/theory/theory_bv_white.h | 6 ++- ...theory_quantifiers_bv_instantiator_white.h | 4 +- .../theory/theory_strings_rewriter_white.h | 4 +- test/unit/theory/theory_white.h | 28 +++++++------- test/unit/theory/type_enumerator_white.h | 9 +++-- test/unit/util/array_store_all_black.h | 6 ++- test/unit/util/binary_heap_black.h | 12 +++--- test/unit/util/bitvector_black.h | 2 +- test/unit/util/datatype_black.h | 9 +++-- test/unit/util/exception_black.h | 12 +++--- test/unit/util/listener_black.h | 12 ++---- test/unit/util/output_black.h | 9 ++--- 42 files changed, 242 insertions(+), 248 deletions(-) diff --git a/test/unit/base/map_util_black.h b/test/unit/base/map_util_black.h index 6d2d2bbc7..39567d6ac 100644 --- a/test/unit/base/map_util_black.h +++ b/test/unit/base/map_util_black.h @@ -38,8 +38,8 @@ using std::string; class MapUtilBlack : public CxxTest::TestSuite { public: - void setUp() {} - void tearDown() {} + void setUp() override {} + void tearDown() override {} // Returns a map containing {"key"->"value", "other"->"entry"}. static const std::map& DefaultMap() diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 7545fa808..8a31f70ca 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -40,9 +40,9 @@ class CDListBlack : public CxxTest::TestSuite { Context* d_context; public: - void setUp() { d_context = new Context(); } + void setUp() override { d_context = new Context(); } - void tearDown() { delete d_context; } + void tearDown() override { delete d_context; } // test at different sizes. this triggers grow() behavior differently. // grow() was completely broken in revision 256 diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 8cc1b73c2..2d2b3f409 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -31,14 +31,15 @@ class CDMapBlack : public CxxTest::TestSuite { Context* d_context; public: - void setUp() { + void setUp() override + { d_context = new Context; // Debug.on("context"); // Debug.on("gc"); // Debug.on("pushpop"); } - void tearDown() { delete d_context; } + void tearDown() override { delete d_context; } // Returns the elements in a CDHashMap. static std::map GetElements(const CDHashMap& map) { diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 232eb55a8..0f111cd61 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -27,17 +27,13 @@ class CDMapWhite : public CxxTest::TestSuite { Context* d_context; -public: + public: + void setUp() override { d_context = new Context; } - void setUp() { - d_context = new Context; - } - - void tearDown() { - delete d_context; - } + void tearDown() override { delete d_context; } - void testUnreachableSaveAndRestore() { + void testUnreachableSaveAndRestore() + { CDHashMap map(d_context); TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index f5666173d..2838ae322 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -33,17 +33,13 @@ private: Context* d_context; -public: + public: + void setUp() override { d_context = new Context; } - void setUp() { - d_context = new Context; - } - - void tearDown() { - delete d_context; - } + void tearDown() override { delete d_context; } - void testIntCDO() { + void testIntCDO() + { // Test that push/pop maintains the original value CDO a1(d_context); a1 = 5; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 63b60edc9..b4be4197c 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -36,12 +36,10 @@ struct MyContextNotifyObj : public ContextNotifyObj { ContextNotifyObj(context, pre), nCalls(0) { } - - virtual ~MyContextNotifyObj() {} - void contextNotifyPop() { - ++nCalls; - } + ~MyContextNotifyObj() override {} + + void contextNotifyPop() override { ++nCalls; } }; class MyContextObj : public ContextObj { @@ -75,18 +73,15 @@ public: nSaves(0) { } - virtual ~MyContextObj() { - destroy(); - } + ~MyContextObj() override { destroy(); } - ContextObj* save(ContextMemoryManager* pcmm) { + ContextObj* save(ContextMemoryManager* pcmm) override + { ++nSaves; return new(pcmm) MyContextObj(*this); } - void restore(ContextObj* contextObj) { - nCalls = notify.nCalls; - } + void restore(ContextObj* contextObj) override { nCalls = notify.nCalls; } void makeCurrent() { ContextObj::makeCurrent(); @@ -99,17 +94,13 @@ private: Context* d_context; -public: + public: + void setUp() override { d_context = new Context; } - void setUp() { - d_context = new Context; - } - - void tearDown() { - delete d_context; - } + void tearDown() override { delete d_context; } - void testContextPushPop() { + void testContextPushPop() + { // Test what happens when the context is popped below 0 // the interface doesn't declare any exceptions d_context->push(); diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index ed64b5eac..beace137e 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -33,13 +33,11 @@ private: ContextMemoryManager* d_cmm; -public: + public: + void setUp() override { d_cmm = new ContextMemoryManager(); } - void setUp() { - d_cmm = new ContextMemoryManager(); - } - - void testPushPop() { + void testPushPop() + { #ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER #warning "Using the debug context memory manager, omitting unit tests" #else @@ -96,7 +94,5 @@ public: #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */ } - void tearDown() { - delete d_cmm; - } + void tearDown() override { delete d_cmm; } }; diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 64e6e184b..2c1ef8e71 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -29,18 +29,14 @@ private: Context* d_context; -public: + public: + void setUp() override { d_context = new Context; } - void setUp() { - d_context = new Context; - } - - void tearDown() { - delete d_context; - } + void tearDown() override { delete d_context; } - void testContextSimple() { - Scope *s = d_context->getTopScope(); + void testContextSimple() + { + Scope* s = d_context->getTopScope(); TS_ASSERT(s == d_context->getBottomScope()); TS_ASSERT(d_context->getLevel() == 0); diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index afc99ef32..58defe07d 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -42,16 +42,17 @@ private: SmtEngine* d_smtEngine; SmtScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_exprManager = new ExprManager(); d_nodeManager = NodeManager::fromExprManager(d_exprManager); d_smtEngine = new SmtEngine(d_exprManager); d_scope = new SmtScope(d_smtEngine); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_smtEngine; delete d_exprManager; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index a169855e2..847cbf929 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -61,9 +61,9 @@ class AttributeWhite : public CxxTest::TestSuite { TypeNode* d_booleanType; SmtEngine* d_smtEngine; -public: - - void setUp() { + public: + void setUp() override + { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smtEngine = new SmtEngine(d_em); @@ -71,7 +71,8 @@ public: d_booleanType = new TypeNode(d_nm->booleanType()); } - void tearDown() { + void tearDown() override + { delete d_booleanType; delete d_scope; delete d_smtEngine; diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index a131aa140..9c604aa52 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -61,19 +61,19 @@ private: return vars; } + public: + void setUp() override { d_exprManager = new ExprManager; } -public: - void setUp() { - d_exprManager = new ExprManager; - } - - - void tearDown() { - try { + void tearDown() override + { + try + { delete d_exprManager; - } catch(Exception e) { + } + catch (Exception e) + { cerr << "Exception during tearDown():" << endl << e; - throw ; + throw; } } diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 4354c5b6a..d8774db82 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -50,12 +50,12 @@ private: Expr* r1; Expr* r2; -public: - - void setUp() { - try { - - char *argv[2]; + public: + void setUp() override + { + try + { + char* argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); Options::parseOptions(&opts, 2, argv); @@ -64,12 +64,13 @@ public: d_em = new ExprManager(opts); - a_bool = new Expr(d_em->mkVar("a",d_em->booleanType())); + a_bool = new Expr(d_em->mkVar("a", d_em->booleanType())); b_bool = new Expr(d_em->mkVar("b", d_em->booleanType())); c_bool_and = new Expr(d_em->mkExpr(AND, *a_bool, *b_bool)); and_op = new Expr(d_em->mkConst(AND)); plus_op = new Expr(d_em->mkConst(PLUS)); - fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType())); + fun_type = new Type( + d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType())); fun_op = new Expr(d_em->mkVar("f", *fun_type)); d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool)); null = new Expr(); @@ -78,13 +79,16 @@ public: i2 = new Expr(d_em->mkConst(Rational(23))); r1 = new Expr(d_em->mkConst(Rational(1, 5))); r2 = new Expr(d_em->mkConst(Rational("0"))); - } catch(Exception e) { + } + catch (Exception e) + { cerr << "Exception during setUp():" << endl << e; throw; } } - void tearDown() { + void tearDown() override + { try { delete r2; delete r1; diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index 5ac503b0e..900f5dac6 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -34,13 +34,15 @@ class KindBlack : public CxxTest::TestSuite { //easier to define in setup int beyond; Kind unknown; -public: - void setUp() { + + public: + void setUp() override + { undefined = UNDEFINED_KIND; null = NULL_EXPR; last = LAST_KIND; - beyond = ((int) LAST_KIND) + 1; - unknown = (Kind) beyond; + beyond = ((int)LAST_KIND) + 1; + unknown = (Kind)beyond; } diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index fb468c896..461d59498 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -56,7 +56,8 @@ class NodeBlack : public CxxTest::TestSuite { TypeNode* d_realType; public: - void setUp() { + void setUp() override + { char* argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); @@ -70,7 +71,8 @@ class NodeBlack : public CxxTest::TestSuite { d_realType = new TypeNode(d_nodeManager->realType()); } - void tearDown() { + void tearDown() override + { delete d_realType; delete d_booleanType; delete d_scope; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index b8e9d92f6..f4fbbb5d9 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -40,9 +40,9 @@ private: TypeNode* d_integerType; TypeNode* d_realType; -public: - - void setUp() { + public: + void setUp() override + { d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); @@ -52,7 +52,8 @@ public: d_realType = new TypeNode(d_nm->realType()); } - void tearDown() { + void tearDown() override + { delete d_integerType; delete d_booleanType; delete d_realType; diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 68c94c176..5da55916b 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -34,14 +34,15 @@ class NodeManagerBlack : public CxxTest::TestSuite { NodeManager* d_nodeManager; NodeManagerScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_nodeManager = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nodeManager); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_nodeManager; } diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index e2b8cbf1c..016ea7793 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -30,14 +30,15 @@ class NodeManagerWhite : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_nm; } diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index bab7e2b0c..cfc4a6b7a 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -33,16 +33,17 @@ private: TypeNode* d_booleanType; TypeNode* d_realType; -public: - - void setUp() { + public: + void setUp() override + { d_nodeManager = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nodeManager); d_booleanType = new TypeNode(d_nodeManager->booleanType()); d_realType = new TypeNode(d_nodeManager->realType()); } - void tearDown() { + void tearDown() override + { delete d_booleanType; delete d_scope; delete d_nodeManager; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index d2d6a265d..09d015e42 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -34,14 +34,15 @@ class NodeWhite : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_nm; } diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 33b5d73c9..2f6f88c27 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -37,18 +37,22 @@ private: ExprManager* d_exprManager; -public: - - void setUp() { - try { + public: + void setUp() override + { + try + { d_exprManager = new ExprManager; - } catch(Exception e) { + } + catch (Exception e) + { cerr << "Exception during setUp():" << endl << e; throw; } } - void tearDown() { + void tearDown() override + { try { delete d_exprManager; } catch(Exception e) { diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index ff05df5da..51cb6a881 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -32,20 +32,20 @@ using namespace std; class TypeCardinalityPublic : public CxxTest::TestSuite { ExprManager* d_em; -public: - - void setUp() { - d_em = new ExprManager(); - } - - void tearDown() { - delete d_em; - } - - void testTheBasics() { - TS_ASSERT( d_em->booleanType().getCardinality().compare(2) == Cardinality::EQUAL ); - TS_ASSERT( d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); - TS_ASSERT( d_em->realType().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + public: + void setUp() override { d_em = new ExprManager(); } + + void tearDown() override { delete d_em; } + + void testTheBasics() + { + TS_ASSERT(d_em->booleanType().getCardinality().compare(2) + == Cardinality::EQUAL); + TS_ASSERT( + d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) + == Cardinality::EQUAL); + TS_ASSERT(d_em->realType().getCardinality().compare(Cardinality::REALS) + == Cardinality::EQUAL); } void testArrays() { diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 45a48ea99..32b5ca7cb 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -37,16 +37,17 @@ class TypeNodeWhite : public CxxTest::TestSuite { NodeManagerScope* d_scope; SmtEngine* d_smt; -public: - - void setUp() { + public: + void setUp() override + { d_em = new ExprManager(); d_nm = d_em->getNodeManager(); d_smt = new SmtEngine(d_em); d_scope = new NodeManagerScope(d_nm); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_smt; delete d_em; diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index 44b3660c9..cf76bb05a 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -35,7 +35,7 @@ using namespace std; class InteractiveShellBlack : public CxxTest::TestSuite { public: - void setUp() + void setUp() override { d_sin = new stringstream; d_sout = new stringstream; @@ -45,7 +45,8 @@ class InteractiveShellBlack : public CxxTest::TestSuite d_solver.reset(new api::Solver(&d_options)); } - void tearDown() { + void tearDown() override + { delete d_sin; delete d_sout; } diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index e7548708e..58ed12a60 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -217,13 +217,9 @@ class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack { public: Cvc4ParserTest() : ParserBlack(LANG_CVC4) { } - void setUp() { - super::setUp(); - } + void setUp() override { super::setUp(); } - void tearDown() { - super::tearDown(); - } + void tearDown() override { super::tearDown(); } void testGoodCvc4Inputs() { tryGoodInput(""); // empty string is OK @@ -307,13 +303,9 @@ class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack { public: Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { } - void setUp() { - super::setUp(); - } + void setUp() override { super::setUp(); } - void tearDown() { - super::tearDown(); - } + void tearDown() override { super::tearDown(); } void testGoodSmt1Inputs() { tryGoodInput(""); // empty string is OK @@ -376,15 +368,12 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack { public: Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { } - void setUp() { - super::setUp(); - } + void setUp() override { super::setUp(); } - void tearDown() { - super::tearDown(); - } + void tearDown() override { super::tearDown(); } - virtual void setupContext(Parser& parser) { + void setupContext(Parser& parser) override + { if(dynamic_cast(&parser) != NULL){ dynamic_cast(&parser)->addTheory(Smt2::THEORY_CORE); } diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 45baf177f..d83d2681b 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -38,9 +38,9 @@ using namespace std; class ParserBuilderBlack : public CxxTest::TestSuite { public: - void setUp() { d_solver.reset(new api::Solver()); } + void setUp() override { d_solver.reset(new api::Solver()); } - void tearDown() {} + void tearDown() override {} void testEmptyFileInput() { diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index 7d7ee1a3a..f238ba8be 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -177,7 +177,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite public: TheoryBVGaussWhite() {} - void setUp() + void setUp() override { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); @@ -251,7 +251,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_z_mul_nine = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine); } - void tearDown() + void tearDown() override { (void)d_scope; d_p = Node::null(); diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index be69a7a1d..7e04bb7c5 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -49,31 +49,34 @@ class FakeSatSolver : public SatSolver { public: FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {} - SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) { + SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override + { return d_nextVar++; } - SatVariable trueVar() { return d_nextVar++; } + SatVariable trueVar() override { return d_nextVar++; } - SatVariable falseVar() { return d_nextVar++; } + SatVariable falseVar() override { return d_nextVar++; } - ClauseId addClause(SatClause& c, bool lemma) { + ClauseId addClause(SatClause& c, bool lemma) override + { d_addClauseCalled = true; return ClauseIdUndef; } - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override + { d_addClauseCalled = true; return ClauseIdUndef; } - bool nativeXor() { return false; } + bool nativeXor() override { return false; } void reset() { d_addClauseCalled = false; } unsigned int addClauseCalled() { return d_addClauseCalled; } - unsigned getAssertionLevel() const { return 0; } + unsigned getAssertionLevel() const override { return 0; } bool isDecision(Node) const { return false; } @@ -83,19 +86,22 @@ class FakeSatSolver : public SatSolver { bool spendResource() { return false; } - void interrupt() {} + void interrupt() override {} - SatValue solve() { return SAT_VALUE_UNKNOWN; } + SatValue solve() override { return SAT_VALUE_UNKNOWN; } - SatValue solve(long unsigned int& resource) { return SAT_VALUE_UNKNOWN; } + SatValue solve(long unsigned int& resource) override + { + return SAT_VALUE_UNKNOWN; + } - SatValue value(SatLiteral l) { return SAT_VALUE_UNKNOWN; } + SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; } - SatValue modelValue(SatLiteral l) { return SAT_VALUE_UNKNOWN; } + SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; } bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; } - bool ok() const { return true; } + bool ok() const override { return true; } }; /* class FakeSatSolver */ @@ -122,7 +128,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { SmtScope* d_scope; SmtEngine* d_smt; - void setUp() { + void setUp() override + { d_exprManager = new ExprManager(); d_smt = new SmtEngine(d_exprManager); d_smt->d_logic.lock(); @@ -138,7 +145,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_satSolver, d_cnfRegistrar, d_cnfContext, d_smt->channels()); } - void tearDown() { + void tearDown() override + { delete d_cnfStream; delete d_cnfContext; delete d_cnfRegistrar; diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index 4416ee00a..10cb15f6f 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -43,7 +43,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite public: TheoryEvaluatorWhite() {} - void setUp() + void setUp() override { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); @@ -53,7 +53,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite d_scope = new SmtScope(d_smt); } - void tearDown() + void tearDown() override { delete d_scope; delete d_smt; diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 2cb1243d5..7661c08b5 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -97,7 +97,8 @@ public: } } - void setUp() { + void setUp() override + { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); @@ -125,7 +126,8 @@ public: } - void tearDown() { + void tearDown() override + { delete d_intType; delete d_realType; delete d_booleanType; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 487c6a434..569d7e30b 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -44,9 +44,9 @@ private: NodeManager* d_nm; SmtScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_em = new ExprManager(); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); @@ -54,7 +54,8 @@ public: d_nm = NodeManager::fromExprManager(d_em); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_smt; delete d_em; diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index c830e7813..bc5b36a0b 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -52,14 +52,16 @@ public: TheoryBVWhite() {} - void setUp() { + void setUp() override + { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_smt; delete d_em; diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 4c96f6cb9..018744bd1 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -38,8 +38,8 @@ using namespace CVC4::smt; class BvInstantiatorWhite : public CxxTest::TestSuite { public: - void setUp(); - void tearDown(); + void setUp() override; + void tearDown() override; void testGetPvCoeff(); void testNormalizePvMult(); diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index fc073b5a4..67dc20541 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -39,7 +39,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite public: TheoryStringsRewriterWhite() {} - void setUp() + void setUp() override { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); @@ -49,7 +49,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite d_scope = new SmtScope(d_smt); } - void tearDown() + void tearDown() override { delete d_scope; delete d_smt; diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 0fbf9c1d6..c8265a755 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -122,20 +122,19 @@ public: return done(); } - void check(Effort e) { + void check(Effort e) override + { while(!done()) { getWrapper(); } } - void presolve() { - Unimplemented(); - } - void preRegisterTerm(TNode n) {} - void propagate(Effort level) {} - Node explain(TNode n) { return Node::null(); } + void presolve() override { Unimplemented(); } + void preRegisterTerm(TNode n) override {} + void propagate(Effort level) override {} + Node explain(TNode n) override { return Node::null(); } Node getValue(TNode n) { return Node::null(); } - string identify() const { return "DummyTheory"; } + string identify() const override { return "DummyTheory"; } };/* class DummyTheory */ class TheoryBlack : public CxxTest::TestSuite { @@ -155,9 +154,9 @@ class TheoryBlack : public CxxTest::TestSuite { Node atom0; Node atom1; -public: - - void setUp() { + public: + void setUp() override + { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); @@ -173,14 +172,15 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; - d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), - *d_logicInfo); + d_dummy = new DummyTheory( + d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); } - void tearDown() { + void tearDown() override + { atom1 = Node::null(); atom0 = Node::null(); delete d_dummy; diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 03b1a2a95..b68941843 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -38,15 +38,16 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_scope = new NodeManagerScope(d_nm); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_em; } diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 49a0b995a..c668e8c8f 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -30,12 +30,14 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite { ExprManagerScope* d_scope; public: - void setUp() { + void setUp() override + { d_em = new ExprManager(); d_scope = new ExprManagerScope(*d_em); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_em; } diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h index 904b78b4b..ce7e854d8 100644 --- a/test/unit/util/binary_heap_black.h +++ b/test/unit/util/binary_heap_black.h @@ -25,20 +25,18 @@ using namespace CVC4; using namespace std; class BinaryHeapBlack : public CxxTest::TestSuite { -public: + public: + void setUp() override {} - void setUp() { - } - - void tearDown() { - } + void tearDown() override {} /** * Test a a series of simple heaps (push a few then pop all then do others). * Done as a series to test if the heap structure falls into a bad state * after prolonged use. */ - void testHeapSeries() { + void testHeapSeries() + { BinaryHeap heap; // First test a heap of 1 element diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index 04fdc4044..c75368196 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -26,7 +26,7 @@ class BitVectorBlack : public CxxTest::TestSuite { public: - void setUp() + void setUp() override { zero = BitVector(4); one = zero.setBit(0); diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 7e69e4efe..c2086c415 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -31,16 +31,17 @@ class DatatypeBlack : public CxxTest::TestSuite { ExprManager* d_em; ExprManagerScope* d_scope; -public: - - void setUp() { + public: + void setUp() override + { d_em = new ExprManager(); d_scope = new ExprManagerScope(*d_em); Debug.on("datatypes"); Debug.on("groundterms"); } - void tearDown() { + void tearDown() override + { delete d_scope; delete d_em; } diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h index 0eb4b0040..ba17d28da 100644 --- a/test/unit/util/exception_black.h +++ b/test/unit/util/exception_black.h @@ -25,16 +25,14 @@ using namespace CVC4; using namespace std; class ExceptionBlack : public CxxTest::TestSuite { -public: + public: + void setUp() override {} - void setUp() { - } - - void tearDown() { - } + void tearDown() override {} // CVC4::Exception is a simple class, just test it all at once. - void testExceptions() { + void testExceptions() + { Exception e1; Exception e2(string("foo!")); Exception e3("bar!"); diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h index 014970b77..7296de060 100644 --- a/test/unit/util/listener_black.h +++ b/test/unit/util/listener_black.h @@ -30,9 +30,9 @@ class ListenerBlack : public CxxTest::TestSuite { public: EventListener(std::multiset& events, std::string name) : d_events(events), d_name(name) {} - ~EventListener(){} + ~EventListener() override {} - virtual void notify() { d_events.insert(d_name); } + void notify() override { d_events.insert(d_name); } private: std::multiset& d_events; @@ -45,13 +45,9 @@ public: return std::multiset(arr, arr + len); } - void setUp() { - d_events.clear(); - } + void setUp() override { d_events.clear(); } - void tearDown() { - d_events.clear(); - } + void tearDown() override { d_events.clear(); } void testEmptyCollection() { // Makes an new collection and tests that it is empty. diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index c8833ced5..cea30f360 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -33,9 +33,9 @@ class OutputBlack : public CxxTest::TestSuite { stringstream d_messageStream; stringstream d_warningStream; -public: - - void setUp() { + public: + void setUp() override + { DebugChannel.setStream(&d_debugStream); TraceChannel.setStream(&d_traceStream); NoticeChannel.setStream(&d_noticeStream); @@ -51,8 +51,7 @@ public: d_warningStream.str(""); } - void tearDown() { - } + void tearDown() override {} void testOutput() { Debug.on("foo"); -- 2.30.2