google test: expr: Migrate symbol_table_black. (#5870)

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 89de279e0399595338b2b1e11c99ae486bf8b2fd..9f39a3b47f3a6afbdb68facb313d88a67397a872 100644 (file)
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -23,6 +23,6 @@ cvc4_add_unit_test_white(node_manager_white expr)
 cvc4_add_cxx_unit_test_black(node_self_iterator_black expr)
 cvc4_add_cxx_unit_test_black(node_traversal_black expr)
 cvc4_add_cxx_unit_test_white(node_white expr)
-cvc4_add_cxx_unit_test_black(symbol_table_black expr)
+cvc4_add_unit_test_black(symbol_table_black expr)
 cvc4_add_cxx_unit_test_black(type_cardinality_public expr)
 cvc4_add_cxx_unit_test_white(type_node_white expr)

diff --git a/test/unit/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp
new file mode 100644 (file)
index 0000000..2897a55
--- /dev/null
+++ b/test/unit/expr/symbol_table_black.cpp
@@ -0,0 +1,153 @@
+/*********************                                                        */
+/*! \file symbol_table_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Christopher L. Conway, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 <cxxtest/TestSuite.h>
+
+#include <sstream>
+#include <string>
+
+#include "base/check.h"
+#include "base/exception.h"
+#include "context/context.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/symbol_table.h"
+#include "expr/type.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestSymbolTableBlack : public TestApi
+{
+};
+
+TEST_F(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, bad_pop)
+{
+  SymbolTable symtab;
+  ASSERT_THROW(symtab.popScope(), ScopeException);
+}
+
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
deleted file mode 100644 (file)
index 4aa1e4f..0000000
--- a/test/unit/expr/symbol_table_black.h
+++ /dev/null
@@ -1,167 +0,0 @@
-/*********************                                                        */
-/*! \file symbol_table_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 <cxxtest/TestSuite.h>
-
-#include <sstream>
-#include <string>
-
-#include "api/cvc4cpp.h"
-#include "base/check.h"
-#include "base/exception.h"
-#include "context/context.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/symbol_table.h"
-#include "expr/type.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace std;
-
-class SymbolTableBlack : public CxxTest::TestSuite {
- public:
-  void setUp() override
-  {
-    try
-    {
-      d_slv = new api::Solver();
-    }
-    catch (Exception& e)
-    {
-      cerr << "Exception during setUp():" << endl << e;
-      throw;
-    }
-  }
-
-  void tearDown() override
-  {
-    try {
-      delete d_slv;
-    }
-    catch (Exception& e)
-    {
-      cerr << "Exception during tearDown():" << endl << e;
-      throw;
-    }
-  }
-
-  void testBind() {
-    SymbolTable symtab;
-    api::Sort booleanType = d_slv->getBooleanSort();
-    api::Term x = d_slv->mkConst(booleanType);
-    symtab.bind("x",x);
-    TS_ASSERT( symtab.isBound("x") );
-    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
-  }
-
-  void testBind2() {
-    SymbolTable symtab;
-    api::Sort booleanType = d_slv->getBooleanSort();
-    // var name attribute shouldn't matter
-    api::Term y = d_slv->mkConst(booleanType, "y");
-    symtab.bind("x",y);
-    TS_ASSERT( symtab.isBound("x") );
-    TS_ASSERT_EQUALS( symtab.lookup("x"), y );
-  }
-
-  void testBind3() {
-    SymbolTable symtab;
-    api::Sort booleanType = d_slv->getBooleanSort();
-    api::Term x = d_slv->mkConst(booleanType);
-    symtab.bind("x",x);
-    api::Term y = d_slv->mkConst(booleanType);
-    // new binding covers old
-    symtab.bind("x",y);
-    TS_ASSERT( symtab.isBound("x") );
-    TS_ASSERT_EQUALS( symtab.lookup("x"), y );
-  }
-
-  void testBind4() {
-    SymbolTable symtab;
-    api::Sort booleanType = d_slv->getBooleanSort();
-    api::Term x = d_slv->mkConst(booleanType);
-    symtab.bind("x",x);
-
-    api::Sort t = d_slv->mkUninterpretedSort("T");
-    // duplicate binding for type is OK
-    symtab.bindType("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() {
-    SymbolTable symtab;
-    api::Sort s = d_slv->mkUninterpretedSort("S");
-    symtab.bindType("S",s);
-    TS_ASSERT( symtab.isBoundType("S") );
-    TS_ASSERT_EQUALS( symtab.lookupType("S"), s );
-  }
-
-  void testBindType2() {
-    SymbolTable symtab;
-    // type name attribute shouldn't matter
-    api::Sort s = d_slv->mkUninterpretedSort("S");
-    symtab.bindType("T",s);
-    TS_ASSERT( symtab.isBoundType("T") );
-    TS_ASSERT_EQUALS( symtab.lookupType("T"), s );
-  }
-
-  void testBindType3() {
-    SymbolTable symtab;
-    api::Sort s = d_slv->mkUninterpretedSort("S");
-    symtab.bindType("S",s);
-    api::Sort t = d_slv->mkUninterpretedSort("T");
-    // new binding covers old
-    symtab.bindType("S",t);
-    TS_ASSERT( symtab.isBoundType("S") );
-    TS_ASSERT_EQUALS( symtab.lookupType("S"), t );
-  }
-
-  void testPushScope() {
-    SymbolTable symtab;
-    api::Sort booleanType = d_slv->getBooleanSort();
-    api::Term x = d_slv->mkConst(booleanType);
-    symtab.bind("x",x);
-    symtab.pushScope();
-
-    TS_ASSERT( symtab.isBound("x") );
-    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
-
-    api::Term y = d_slv->mkConst(booleanType);
-    symtab.bind("x",y);
-
-    TS_ASSERT( symtab.isBound("x") );
-    TS_ASSERT_EQUALS( symtab.lookup("x"), y );
-
-    symtab.popScope();
-    TS_ASSERT( symtab.isBound("x") );
-    TS_ASSERT_EQUALS( symtab.lookup("x"), x );
-  }
-
-  void testBadPop() {
-    SymbolTable symtab;
-    // TODO: What kind of exception gets thrown here?
-    TS_ASSERT_THROWS(symtab.popScope(), ScopeException&);
-  }
-
- private:
-  api::Solver* d_slv;
-};/* class SymbolTableBlack */