Merging from branches/decl-scopes (r401:411)

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);
   }