diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-17 11:07:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-17 18:07:48 +0000 |
commit | bbf9eee55db6851c0923252cdda8946030c3c75a (patch) | |
tree | 52d3f04010f61784a3494e5de27d6e70c20b9abb /test/unit/node/symbol_table_black.cpp | |
parent | fe72d5a3fce499092c842b48df997eb0aa54fc05 (diff) |
Rename test/unit/expr to test/unit/node. (#6156)
This is in preparation for renaming src/expr to src/node.
Diffstat (limited to 'test/unit/node/symbol_table_black.cpp')
-rw-r--r-- | test/unit/node/symbol_table_black.cpp | 149 |
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 |