1 files changed, 149 insertions, 0 deletions
diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp
new file mode 100644
index 000000000..c1865eaa9
--- /dev/null
+++ b/test/unit/node/symbol_table_black.cpp
@@ -0,0 +1,149 @@
+/*********************                                                        */
+/*! \file symbol_table_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters, Christopher L. Conway
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::SymbolTable
+ **
+ ** Black box testing of CVC4::SymbolTable.
+ **/
+
+#include <sstream>
+#include <string>
+
+#include "base/check.h"
+#include "base/exception.h"
+#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/symbol_table.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestNodeBlackSymbolTable : public TestApi
+{
+};
+
+TEST_F(TestNodeBlackSymbolTable, bind1)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind2)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  // var name attribute shouldn't matter
+  api::Term y = d_solver.mkConst(booleanType, "y");
+  symtab.bind("x", y);
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), y);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind3)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+  api::Term y = d_solver.mkConst(booleanType);
+  // new binding covers old
+  symtab.bind("x", y);
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), y);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind4)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+
+  api::Sort t = d_solver.mkUninterpretedSort("T");
+  // duplicate binding for type is OK
+  symtab.bindType("x", t);
+
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+  ASSERT_TRUE(symtab.isBoundType("x"));
+  ASSERT_EQ(symtab.lookupType("x"), t);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type1)
+{
+  SymbolTable symtab;
+  api::Sort s = d_solver.mkUninterpretedSort("S");
+  symtab.bindType("S", s);
+  ASSERT_TRUE(symtab.isBoundType("S"));
+  ASSERT_EQ(symtab.lookupType("S"), s);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type2)
+{
+  SymbolTable symtab;
+  // type name attribute shouldn't matter
+  api::Sort s = d_solver.mkUninterpretedSort("S");
+  symtab.bindType("T", s);
+  ASSERT_TRUE(symtab.isBoundType("T"));
+  ASSERT_EQ(symtab.lookupType("T"), s);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type3)
+{
+  SymbolTable symtab;
+  api::Sort s = d_solver.mkUninterpretedSort("S");
+  symtab.bindType("S", s);
+  api::Sort t = d_solver.mkUninterpretedSort("T");
+  // new binding covers old
+  symtab.bindType("S", t);
+  ASSERT_TRUE(symtab.isBoundType("S"));
+  ASSERT_EQ(symtab.lookupType("S"), t);
+}
+
+TEST_F(TestNodeBlackSymbolTable, push_scope)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+  symtab.pushScope();
+
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+
+  api::Term y = d_solver.mkConst(booleanType);
+  symtab.bind("x", y);
+
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), y);
+
+  symtab.popScope();
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bad_pop)
+{
+  SymbolTable symtab;
+  ASSERT_THROW(symtab.popScope(), ScopeException);
+}
+
+}  // namespace test
+}  // namespace CVC4