GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/symbol_table_black.cpp Lines: 74 74 100.0 %
Date: 2021-03-22 Branches: 203 590 34.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file symbol_table_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters, Christopher L. Conway
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::SymbolTable
13
 **
14
 ** Black box testing of CVC4::SymbolTable.
15
 **/
16
17
#include <sstream>
18
#include <string>
19
20
#include "base/check.h"
21
#include "base/exception.h"
22
#include "context/context.h"
23
#include "expr/kind.h"
24
#include "expr/symbol_table.h"
25
#include "test_api.h"
26
27
namespace CVC4 {
28
29
using namespace kind;
30
using namespace context;
31
32
namespace test {
33
34
36
class TestNodeBlackSymbolTable : public TestApi
35
{
36
};
37
38
18
TEST_F(TestNodeBlackSymbolTable, bind1)
39
{
40
4
  SymbolTable symtab;
41
4
  api::Sort booleanType = d_solver.getBooleanSort();
42
4
  api::Term x = d_solver.mkConst(booleanType);
43
2
  symtab.bind("x", x);
44
2
  ASSERT_TRUE(symtab.isBound("x"));
45
2
  ASSERT_EQ(symtab.lookup("x"), x);
46
}
47
48
18
TEST_F(TestNodeBlackSymbolTable, bind2)
49
{
50
4
  SymbolTable symtab;
51
4
  api::Sort booleanType = d_solver.getBooleanSort();
52
  // var name attribute shouldn't matter
53
4
  api::Term y = d_solver.mkConst(booleanType, "y");
54
2
  symtab.bind("x", y);
55
2
  ASSERT_TRUE(symtab.isBound("x"));
56
2
  ASSERT_EQ(symtab.lookup("x"), y);
57
}
58
59
18
TEST_F(TestNodeBlackSymbolTable, bind3)
60
{
61
4
  SymbolTable symtab;
62
4
  api::Sort booleanType = d_solver.getBooleanSort();
63
4
  api::Term x = d_solver.mkConst(booleanType);
64
2
  symtab.bind("x", x);
65
4
  api::Term y = d_solver.mkConst(booleanType);
66
  // new binding covers old
67
2
  symtab.bind("x", y);
68
2
  ASSERT_TRUE(symtab.isBound("x"));
69
2
  ASSERT_EQ(symtab.lookup("x"), y);
70
}
71
72
18
TEST_F(TestNodeBlackSymbolTable, bind4)
73
{
74
4
  SymbolTable symtab;
75
4
  api::Sort booleanType = d_solver.getBooleanSort();
76
4
  api::Term x = d_solver.mkConst(booleanType);
77
2
  symtab.bind("x", x);
78
79
4
  api::Sort t = d_solver.mkUninterpretedSort("T");
80
  // duplicate binding for type is OK
81
2
  symtab.bindType("x", t);
82
83
2
  ASSERT_TRUE(symtab.isBound("x"));
84
2
  ASSERT_EQ(symtab.lookup("x"), x);
85
2
  ASSERT_TRUE(symtab.isBoundType("x"));
86
2
  ASSERT_EQ(symtab.lookupType("x"), t);
87
}
88
89
18
TEST_F(TestNodeBlackSymbolTable, bind_type1)
90
{
91
4
  SymbolTable symtab;
92
4
  api::Sort s = d_solver.mkUninterpretedSort("S");
93
2
  symtab.bindType("S", s);
94
2
  ASSERT_TRUE(symtab.isBoundType("S"));
95
2
  ASSERT_EQ(symtab.lookupType("S"), s);
96
}
97
98
18
TEST_F(TestNodeBlackSymbolTable, bind_type2)
99
{
100
4
  SymbolTable symtab;
101
  // type name attribute shouldn't matter
102
4
  api::Sort s = d_solver.mkUninterpretedSort("S");
103
2
  symtab.bindType("T", s);
104
2
  ASSERT_TRUE(symtab.isBoundType("T"));
105
2
  ASSERT_EQ(symtab.lookupType("T"), s);
106
}
107
108
18
TEST_F(TestNodeBlackSymbolTable, bind_type3)
109
{
110
4
  SymbolTable symtab;
111
4
  api::Sort s = d_solver.mkUninterpretedSort("S");
112
2
  symtab.bindType("S", s);
113
4
  api::Sort t = d_solver.mkUninterpretedSort("T");
114
  // new binding covers old
115
2
  symtab.bindType("S", t);
116
2
  ASSERT_TRUE(symtab.isBoundType("S"));
117
2
  ASSERT_EQ(symtab.lookupType("S"), t);
118
}
119
120
18
TEST_F(TestNodeBlackSymbolTable, push_scope)
121
{
122
4
  SymbolTable symtab;
123
4
  api::Sort booleanType = d_solver.getBooleanSort();
124
4
  api::Term x = d_solver.mkConst(booleanType);
125
2
  symtab.bind("x", x);
126
2
  symtab.pushScope();
127
128
2
  ASSERT_TRUE(symtab.isBound("x"));
129
2
  ASSERT_EQ(symtab.lookup("x"), x);
130
131
4
  api::Term y = d_solver.mkConst(booleanType);
132
2
  symtab.bind("x", y);
133
134
2
  ASSERT_TRUE(symtab.isBound("x"));
135
2
  ASSERT_EQ(symtab.lookup("x"), y);
136
137
2
  symtab.popScope();
138
2
  ASSERT_TRUE(symtab.isBound("x"));
139
2
  ASSERT_EQ(symtab.lookup("x"), x);
140
}
141
142
18
TEST_F(TestNodeBlackSymbolTable, bad_pop)
143
{
144
4
  SymbolTable symtab;
145
4
  ASSERT_THROW(symtab.popScope(), ScopeException);
146
}
147
148
}  // namespace test
149
30
}  // namespace CVC4