1 /********************* */
2 /*! \file symbol_table.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Christopher L. Conway
6 ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Convenience class for scoping variable and type
13 ** declarations (implementation)
15 ** Convenience class for scoping variable and type declarations
19 #include "expr/symbol_table.h"
20 #include "expr/expr.h"
21 #include "expr/type.h"
22 #include "expr/expr_manager_scope.h"
23 #include "context/cdhashmap.h"
24 #include "context/cdhashset.h"
25 #include "context/context.h"
31 using namespace CVC4::context
;
36 SymbolTable::SymbolTable() :
37 d_context(new Context()),
38 d_exprMap(new(true) CDHashMap
<std::string
, Expr
, StringHashFunction
>(d_context
)),
39 d_typeMap(new(true) CDHashMap
<std::string
, pair
<vector
<Type
>, Type
>, StringHashFunction
>(d_context
)),
40 d_functions(new(true) CDHashSet
<Expr
, ExprHashFunction
>(d_context
)) {
43 SymbolTable::~SymbolTable() {
44 d_exprMap
->deleteSelf();
45 d_typeMap
->deleteSelf();
46 d_functions
->deleteSelf();
50 void SymbolTable::bind(const std::string
& name
, Expr obj
,
51 bool levelZero
) throw() {
52 CheckArgument(!obj
.isNull(), obj
, "cannot bind to a null Expr");
53 ExprManagerScope
ems(obj
);
54 if(levelZero
) d_exprMap
->insertAtContextLevelZero(name
, obj
);
55 else d_exprMap
->insert(name
, obj
);
58 void SymbolTable::bindDefinedFunction(const std::string
& name
, Expr obj
,
59 bool levelZero
) throw() {
60 CheckArgument(!obj
.isNull(), obj
, "cannot bind to a null Expr");
61 ExprManagerScope
ems(obj
);
63 d_exprMap
->insertAtContextLevelZero(name
, obj
);
64 d_functions
->insertAtContextLevelZero(obj
);
66 d_exprMap
->insert(name
, obj
);
67 d_functions
->insert(obj
);
71 bool SymbolTable::isBound(const std::string
& name
) const throw() {
72 return d_exprMap
->find(name
) != d_exprMap
->end();
75 bool SymbolTable::isBoundDefinedFunction(const std::string
& name
) const throw() {
76 CDHashMap
<std::string
, Expr
, StringHashFunction
>::iterator found
=
77 d_exprMap
->find(name
);
78 return found
!= d_exprMap
->end() && d_functions
->contains((*found
).second
);
81 bool SymbolTable::isBoundDefinedFunction(Expr func
) const throw() {
82 return d_functions
->contains(func
);
85 Expr
SymbolTable::lookup(const std::string
& name
) const throw() {
86 return (*d_exprMap
->find(name
)).second
;
89 void SymbolTable::bindType(const std::string
& name
, Type t
,
90 bool levelZero
) throw() {
92 d_typeMap
->insertAtContextLevelZero(name
, make_pair(vector
<Type
>(), t
));
94 d_typeMap
->insert(name
, make_pair(vector
<Type
>(), t
));
98 void SymbolTable::bindType(const std::string
& name
,
99 const std::vector
<Type
>& params
,
101 bool levelZero
) throw() {
102 if(Debug
.isOn("sort")) {
103 Debug("sort") << "bindType(" << name
<< ", [";
104 if(params
.size() > 0) {
105 copy( params
.begin(), params
.end() - 1,
106 ostream_iterator
<Type
>(Debug("sort"), ", ") );
107 Debug("sort") << params
.back();
109 Debug("sort") << "], " << t
<< ")" << endl
;
112 d_typeMap
->insertAtContextLevelZero(name
, make_pair(params
, t
));
114 d_typeMap
->insert(name
, make_pair(params
, t
));
118 bool SymbolTable::isBoundType(const std::string
& name
) const throw() {
119 return d_typeMap
->find(name
) != d_typeMap
->end();
122 Type
SymbolTable::lookupType(const std::string
& name
) const throw() {
123 pair
<vector
<Type
>, Type
> p
= (*d_typeMap
->find(name
)).second
;
124 CheckArgument(p
.first
.size() == 0, name
,
125 "type constructor arity is wrong: "
126 "`%s' requires %u parameters but was provided 0",
127 name
.c_str(), p
.first
.size());
131 Type
SymbolTable::lookupType(const std::string
& name
,
132 const std::vector
<Type
>& params
) const throw() {
133 pair
<vector
<Type
>, Type
> p
= (*d_typeMap
->find(name
)).second
;
134 CheckArgument(p
.first
.size() == params
.size(), params
,
135 "type constructor arity is wrong: "
136 "`%s' requires %u parameters but was provided %u",
137 name
.c_str(), p
.first
.size(), params
.size());
138 if(p
.first
.size() == 0) {
139 CheckArgument(p
.second
.isSort(), name
);
142 if(p
.second
.isSortConstructor()) {
143 if(Debug
.isOn("sort")) {
144 Debug("sort") << "instantiating using a sort constructor" << endl
;
145 Debug("sort") << "have formals [";
146 copy( p
.first
.begin(), p
.first
.end() - 1,
147 ostream_iterator
<Type
>(Debug("sort"), ", ") );
148 Debug("sort") << p
.first
.back() << "]" << endl
150 copy( params
.begin(), params
.end() - 1,
151 ostream_iterator
<Type
>(Debug("sort"), ", ") );
152 Debug("sort") << params
.back() << "]" << endl
153 << "type ctor " << name
<< endl
154 << "type is " << p
.second
<< endl
;
158 SortConstructorType(p
.second
).instantiate(params
);
160 Debug("sort") << "instance is " << instantiation
<< endl
;
162 return instantiation
;
163 } else if(p
.second
.isDatatype()) {
164 CheckArgument(DatatypeType(p
.second
).isParametric(), name
, "expected parametric datatype");
165 return DatatypeType(p
.second
).instantiate(params
);
167 if(Debug
.isOn("sort")) {
168 Debug("sort") << "instantiating using a sort substitution" << endl
;
169 Debug("sort") << "have formals [";
170 copy( p
.first
.begin(), p
.first
.end() - 1,
171 ostream_iterator
<Type
>(Debug("sort"), ", ") );
172 Debug("sort") << p
.first
.back() << "]" << endl
174 copy( params
.begin(), params
.end() - 1,
175 ostream_iterator
<Type
>(Debug("sort"), ", ") );
176 Debug("sort") << params
.back() << "]" << endl
177 << "type ctor " << name
<< endl
178 << "type is " << p
.second
<< endl
;
181 Type instantiation
= p
.second
.substitute(p
.first
, params
);
183 Debug("sort") << "instance is " << instantiation
<< endl
;
185 return instantiation
;
189 size_t SymbolTable::lookupArity(const std::string
& name
) {
190 pair
<vector
<Type
>, Type
> p
= (*d_typeMap
->find(name
)).second
;
191 return p
.first
.size();
194 void SymbolTable::popScope() throw(ScopeException
) {
195 if( d_context
->getLevel() == 0 ) {
196 throw ScopeException();
201 void SymbolTable::pushScope() throw() {
205 size_t SymbolTable::getLevel() const throw() {
206 return d_context
->getLevel();
209 void SymbolTable::reset() {
210 this->SymbolTable::~SymbolTable();
211 new(this) SymbolTable();
214 }/* CVC4 namespace */