From: Aina Niemetz Date: Fri, 5 Feb 2021 22:32:33 +0000 (-0800) Subject: google test: expr: Migrate symbol_table_black. (#5870) X-Git-Tag: cvc5-1.0.0~2314 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7c86d698dad7180096ec2c81012a3ee18d2b94f9;p=cvc5.git google test: expr: Migrate symbol_table_black. (#5870) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 89de279e0..9f39a3b47 100644 --- 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 index 000000000..2897a5588 --- /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 + +#include +#include + +#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 index 4aa1e4f65..000000000 --- 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 - -#include -#include - -#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 */