diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-07 18:38:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-07 18:38:49 +0000 |
commit | b0deae79d8bae5051a85dc15e43e7b83bc8cf9ab (patch) | |
tree | d73fa7f9fb37077853f824dcecd2a1b8e4d22837 /test/unit | |
parent | ea5acaba821790dd240db779f2340fbe5fce0b8e (diff) |
Some items from the CVC4 public interface review:
* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 3 | ||||
-rw-r--r-- | test/unit/context/cdcirclist_white.h | 223 | ||||
-rw-r--r-- | test/unit/expr/symbol_table_black.h (renamed from test/unit/expr/declaration_scope_black.h) | 104 |
3 files changed, 53 insertions, 277 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 88d21cac5..470fdac3d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -17,7 +17,7 @@ UNIT_TESTS = \ expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ - expr/declaration_scope_black \ + expr/symbol_table_black \ expr/node_self_iterator_black \ expr/type_cardinality_public \ expr/type_node_white \ @@ -30,7 +30,6 @@ UNIT_TESTS = \ context/cdo_black \ context/cdlist_black \ context/cdlist_context_memory_black \ - context/cdcirclist_white \ context/cdmap_black \ context/cdmap_white \ context/cdvector_black \ diff --git a/test/unit/context/cdcirclist_white.h b/test/unit/context/cdcirclist_white.h deleted file mode 100644 index b03a850a8..000000000 --- a/test/unit/context/cdcirclist_white.h +++ /dev/null @@ -1,223 +0,0 @@ -/********************* */ -/*! \file cdcirclist_white.h - ** \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 White box testing of CVC4::context::CDCircList<>. - ** - ** White box testing of CVC4::context::CDCircList<>. - **/ - -#include <cxxtest/TestSuite.h> - -#include <vector> -#include <iostream> - -#include <limits.h> - -#include "context/context.h" -#include "context/cdcirclist.h" - -#include "util/output.h" - -using namespace std; -using namespace CVC4::context; -using namespace CVC4; - -class CDCircListWhite : public CxxTest::TestSuite { -private: - - Context* d_context; - -public: - - void setUp() { - d_context = new Context(); - } - - void tearDown() { - delete d_context; - } - - void testSimple() { - //Debug.on("cdcirclist"); - CDCircList<int> l(d_context, ContextMemoryAllocator<int>(d_context->getCMM())); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - d_context->push(); - { - TS_ASSERT(l.empty()); - l.push_back(1); - TS_ASSERT(!l.empty()); - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 1); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - l.push_back(2); - TS_ASSERT(!l.empty()); - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 2); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - l.push_back(3); - TS_ASSERT(!l.empty()); - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 3); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( l.concat(l), AssertionException ); -#endif /* CVC4_ASSERTIONS */ - - CDCircList<int> l2(d_context, ContextMemoryAllocator<int>(d_context->getCMM())); - l2.push_back(4); - l2.push_back(5); - l2.push_back(6); - TS_ASSERT_EQUALS(l2.front(), 4); - TS_ASSERT_EQUALS(l2.back(), 6); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - - d_context->push(); - { - l.concat(l2); - - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 6); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - TS_ASSERT_EQUALS(l2.front(), 4); - TS_ASSERT_EQUALS(l2.back(), 3); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - - d_context->push(); - { - CDCircList<int>::iterator i = l.begin(); - CDCircList<int>::iterator j = l.begin(); - TS_ASSERT_EQUALS(i, j); - TS_ASSERT_EQUALS(i++, j); - TS_ASSERT_EQUALS(i, ++j); - TS_ASSERT_EQUALS(l.erase(l.begin()), i); - - i = l.begin(); - TS_ASSERT_EQUALS(i, j); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(i, l.begin()); TS_ASSERT_EQUALS(i, j); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - } - d_context->pop(); - - CDCircList<int>::iterator i = l.begin(); - TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(i, l.begin()); - - i = l2.begin(); - TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(i, l2.begin()); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - } - d_context->pop(); - - TS_ASSERT(! l.empty()); - TS_ASSERT(! l2.empty()); - - CDCircList<int>::iterator i = l.begin(); - TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(i, l.begin()); - - i = l2.begin(); - TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(i, l2.begin()); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - } - d_context->pop(); - - TS_ASSERT(l.empty()); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - } - - void testCDPtr() { - int* x = (int*)0x12345678; - int* y = (int*)0x87654321; - CDPtr<int> p(d_context, NULL); - TS_ASSERT(p == NULL); - d_context->push(); - TS_ASSERT(p == NULL); - d_context->push(); - TS_ASSERT(p == NULL); - p = x; - TS_ASSERT(p == x); - d_context->push(); - TS_ASSERT(p == x); - p = y; - TS_ASSERT(p == y); - d_context->pop(); - TS_ASSERT(p == x); - d_context->pop(); - TS_ASSERT(p == NULL); - d_context->pop(); - TS_ASSERT(p == NULL); - } - -};/* class CDCircListWhite */ diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/symbol_table_black.h index bde04157c..89fbf42e8 100644 --- a/test/unit/expr/declaration_scope_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file declaration_scope_black.h +/*! \file symbol_table_black.h ** \verbatim ** Original author: cconway ** Major contributors: none @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Black box testing of CVC4::DeclarationScope. + ** \brief Black box testing of CVC4::SymbolTable ** - ** Black box testing of CVC4::DeclarationScope. + ** Black box testing of CVC4::SymbolTable. **/ #include <cxxtest/TestSuite.h> @@ -22,7 +22,7 @@ #include <string> #include "context/context.h" -#include "expr/declaration_scope.h" +#include "expr/symbol_table.h" #include "expr/expr_manager.h" #include "expr/expr.h" #include "expr/type.h" @@ -34,7 +34,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace std; -class DeclarationScopeBlack : public CxxTest::TestSuite { +class SymbolTableBlack : public CxxTest::TestSuite { private: ExprManager* d_exprManager; @@ -60,104 +60,104 @@ public: } void testBind() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + symtab.bind("x",x); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); } void testBind2() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); // var name attribute shouldn't matter Expr y = d_exprManager->mkVar("y", booleanType); - declScope.bind("x",y); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + symtab.bind("x",y); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), y ); } void testBind3() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); + symtab.bind("x",x); Expr y = d_exprManager->mkVar(booleanType); // new binding covers old - declScope.bind("x",y); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + symtab.bind("x",y); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), y ); } void testBind4() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); + symtab.bind("x",x); Type t = d_exprManager->mkSort("T"); // duplicate binding for type is OK - declScope.bindType("x",t); + symtab.bindType("x",t); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); - TS_ASSERT( declScope.isBoundType("x") ); - TS_ASSERT_EQUALS( declScope.lookupType("x"), t ); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); + TS_ASSERT( symtab.isBoundType("x") ); + TS_ASSERT_EQUALS( symtab.lookupType("x"), t ); } void testBindType() { - DeclarationScope declScope; + SymbolTable symtab; Type s = d_exprManager->mkSort("S"); - declScope.bindType("S",s); - TS_ASSERT( declScope.isBoundType("S") ); - TS_ASSERT_EQUALS( declScope.lookupType("S"), s ); + symtab.bindType("S",s); + TS_ASSERT( symtab.isBoundType("S") ); + TS_ASSERT_EQUALS( symtab.lookupType("S"), s ); } void testBindType2() { - DeclarationScope declScope; + SymbolTable symtab; // type name attribute shouldn't matter Type s = d_exprManager->mkSort("S"); - declScope.bindType("T",s); - TS_ASSERT( declScope.isBoundType("T") ); - TS_ASSERT_EQUALS( declScope.lookupType("T"), s ); + symtab.bindType("T",s); + TS_ASSERT( symtab.isBoundType("T") ); + TS_ASSERT_EQUALS( symtab.lookupType("T"), s ); } void testBindType3() { - DeclarationScope declScope; + SymbolTable symtab; Type s = d_exprManager->mkSort("S"); - declScope.bindType("S",s); + symtab.bindType("S",s); Type t = d_exprManager->mkSort("T"); // new binding covers old - declScope.bindType("S",t); - TS_ASSERT( declScope.isBoundType("S") ); - TS_ASSERT_EQUALS( declScope.lookupType("S"), t ); + symtab.bindType("S",t); + TS_ASSERT( symtab.isBoundType("S") ); + TS_ASSERT_EQUALS( symtab.lookupType("S"), t ); } void testPushScope() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); - declScope.pushScope(); + symtab.bind("x",x); + symtab.pushScope(); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); Expr y = d_exprManager->mkVar(booleanType); - declScope.bind("x",y); + symtab.bind("x",y); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), y ); - declScope.popScope(); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + symtab.popScope(); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); } void testBadPop() { - DeclarationScope declScope; + SymbolTable symtab; // TODO: What kind of exception gets thrown here? - TS_ASSERT_THROWS( declScope.popScope(), ScopeException ); + TS_ASSERT_THROWS( symtab.popScope(), ScopeException ); } -}; +};/* class SymbolTableBlack */ |