diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/expr/declaration_scope_black.h | 158 | ||||
-rw-r--r-- | test/unit/parser/parser_white.h | 6 |
3 files changed, 165 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3f0816560..a190152d3 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -9,6 +9,7 @@ UNIT_TESTS = \ expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ + expr/declaration_scope_black \ parser/parser_white \ context/context_black \ context/context_white \ diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h new file mode 100644 index 000000000..f93a3fcc8 --- /dev/null +++ b/test/unit/expr/declaration_scope_black.h @@ -0,0 +1,158 @@ +/********************* */ +/** declaration_scope_black.h + ** Original author: cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Black box testing of CVC4::DeclarationScope. + **/ + +#include <cxxtest/TestSuite.h> + +#include <sstream> +#include <string> + +#include "context/context.h" +#include "expr/declaration_scope.h" +#include "expr/expr_manager.h" +#include "expr/expr.h" +#include "expr/type.h" +#include "util/Assert.h" +#include "util/exception.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace std; + +class DeclarationScopeBlack : public CxxTest::TestSuite { +private: + + ExprManager* d_exprManager; + +public: + + void setUp() { + try { + d_exprManager = new ExprManager; + } catch(Exception e) { + cerr << "Exception during setUp():" << endl << e; + throw; + } + } + + void tearDown() { + try { + delete d_exprManager; + } catch(Exception e) { + cerr << "Exception during tearDown():" << endl << e; + throw; + } + } + + void testBind() { + DeclarationScope declScope; + 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 ); + } + + void testBind2() { + DeclarationScope declScope; + 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 ); + } + + void testBind3() { + DeclarationScope declScope; + Type *booleanType = d_exprManager->booleanType(); + Expr x = d_exprManager->mkVar(booleanType); + declScope.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 ); + } + + void testBind4() { + DeclarationScope declScope; + Type *booleanType = d_exprManager->booleanType(); + Expr x = d_exprManager->mkVar(booleanType); + declScope.bind("x",x); + + Type *t = d_exprManager->mkSort("T"); + // duplicate binding for type is OK + declScope.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 ); + } + + void testBindType() { + DeclarationScope declScope; + Type *s = d_exprManager->mkSort("S"); + declScope.bindType("S",s); + TS_ASSERT( declScope.isBoundType("S") ); + TS_ASSERT_EQUALS( declScope.lookupType("S"), s ); + } + + void testBindType2() { + DeclarationScope declScope; + // 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 ); + } + + void testBindType3() { + DeclarationScope declScope; + Type *s = d_exprManager->mkSort("S"); + declScope.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 ); + } + + void testPushScope() { + DeclarationScope declScope; + Type *booleanType = d_exprManager->booleanType(); + Expr x = d_exprManager->mkVar(booleanType); + declScope.bind("x",x); + declScope.pushScope(); + + TS_ASSERT( declScope.isBound("x") ); + TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + + Expr y = d_exprManager->mkVar(booleanType); + declScope.bind("x",y); + + TS_ASSERT( declScope.isBound("x") ); + TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + + declScope.popScope(); + TS_ASSERT( declScope.isBound("x") ); + TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + } + + void testBadPop() { + DeclarationScope declScope; + // TODO: What kind of exception gets thrown here? + TS_ASSERT_THROWS( declScope.popScope(), ScopeException ); + } +}; diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index d0959cf6f..653e3a1d7 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -261,6 +261,12 @@ public: delete d_exprManager; } + void testBs() { + DeclarationScope declScope; + declScope.bind("foo", d_exprManager->mkVar("foo",d_exprManager->booleanType())); + + } + void testGoodCvc4Inputs() { tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); } |