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