src/expr/symbol_table.cpp

   1 /*********************                                                        */
   2 /*! \file symbol_table.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Christopher L. Conway, Francois Bobot
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 Convenience class for scoping variable and type
  13  ** declarations (implementation)
  14  **
  15  ** Convenience class for scoping variable and type declarations
  16  ** (implementation).
  17  **/
  18
  19 #include "expr/symbol_table.h"
  20
  21 #include <ostream>
  22 #include <string>
  23 #include <utility>
  24
  25 #include "context/cdhashmap.h"
  26 #include "context/cdhashset.h"
  27 #include "context/context.h"
  28 #include "expr/expr.h"
  29 #include "expr/expr_manager_scope.h"
  30 #include "expr/type.h"
  31
  32 namespace CVC4 {
  33
  34 using ::CVC4::context::CDHashMap;
  35 using ::CVC4::context::CDHashSet;
  36 using ::CVC4::context::Context;
  37 using ::std::copy;
  38 using ::std::endl;
  39 using ::std::ostream_iterator;
  40 using ::std::pair;
  41 using ::std::string;
  42 using ::std::vector;
  43
  44 class SymbolTable::Implementation {
  45  public:
  46   Implementation()
  47       : d_context(),
  48         d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
  49         d_typeMap(new (true) TypeMap(&d_context)),
  50         d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {}
  51
  52   void bind(const string& name, Expr obj, bool levelZero) throw();
  53   void bindDefinedFunction(const string& name, Expr obj,
  54                            bool levelZero) throw();
  55   void bindType(const string& name, Type t, bool levelZero = false) throw();
  56   void bindType(const string& name, const vector<Type>& params, Type t,
  57                 bool levelZero = false) throw();
  58   bool isBound(const string& name) const throw();
  59   bool isBoundDefinedFunction(const string& name) const throw();
  60   bool isBoundDefinedFunction(Expr func) const throw();
  61   bool isBoundType(const string& name) const throw();
  62   Expr lookup(const string& name) const throw();
  63   Type lookupType(const string& name) const throw();
  64   Type lookupType(const string& name, const vector<Type>& params) const throw();
  65   size_t lookupArity(const string& name);
  66   void popScope() throw(ScopeException);
  67   void pushScope() throw();
  68   size_t getLevel() const throw();
  69   void reset();
  70
  71  private:
  72   /** The context manager for the scope maps. */
  73   Context d_context;
  74
  75   /** A map for expressions. */
  76   CDHashMap<string, Expr>* d_exprMap;
  77
  78   /** A map for types. */
  79   using TypeMap = CDHashMap<string, std::pair<vector<Type>, Type>>;
  80   TypeMap* d_typeMap;
  81
  82   /** A set of defined functions. */
  83   CDHashSet<Expr, ExprHashFunction>* d_functions;
  84 }; /* SymbolTable::Implementation */
  85
  86 void SymbolTable::Implementation::bind(const string& name, Expr obj,
  87                                        bool levelZero) throw() {
  88   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
  89   ExprManagerScope ems(obj);
  90   if (levelZero) {
  91     d_exprMap->insertAtContextLevelZero(name, obj);
  92   } else {
  93     d_exprMap->insert(name, obj);
  94   }
  95 }
  96
  97 void SymbolTable::Implementation::bindDefinedFunction(const string& name,
  98                                                       Expr obj,
  99                                                       bool levelZero) throw() {
 100   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
 101   ExprManagerScope ems(obj);
 102   if (levelZero) {
 103     d_exprMap->insertAtContextLevelZero(name, obj);
 104     d_functions->insertAtContextLevelZero(obj);
 105   } else {
 106     d_exprMap->insert(name, obj);
 107     d_functions->insert(obj);
 108   }
 109 }
 110
 111 bool SymbolTable::Implementation::isBound(const string& name) const throw() {
 112   return d_exprMap->find(name) != d_exprMap->end();
 113 }
 114
 115 bool SymbolTable::Implementation::isBoundDefinedFunction(
 116     const string& name) const throw() {
 117   CDHashMap<string, Expr>::iterator found = d_exprMap->find(name);
 118   return found != d_exprMap->end() && d_functions->contains((*found).second);
 119 }
 120
 121 bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const
 122     throw() {
 123   return d_functions->contains(func);
 124 }
 125
 126 Expr SymbolTable::Implementation::lookup(const string& name) const throw() {
 127   return (*d_exprMap->find(name)).second;
 128 }
 129
 130 void SymbolTable::Implementation::bindType(const string& name, Type t,
 131                                            bool levelZero) throw() {
 132   if (levelZero) {
 133     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
 134   } else {
 135     d_typeMap->insert(name, make_pair(vector<Type>(), t));
 136   }
 137 }
 138
 139 void SymbolTable::Implementation::bindType(const string& name,
 140                                            const vector<Type>& params, Type t,
 141                                            bool levelZero) throw() {
 142   if (Debug.isOn("sort")) {
 143     Debug("sort") << "bindType(" << name << ", [";
 144     if (params.size() > 0) {
 145       copy(params.begin(), params.end() - 1,
 146            ostream_iterator<Type>(Debug("sort"), ", "));
 147       Debug("sort") << params.back();
 148     }
 149     Debug("sort") << "], " << t << ")" << endl;
 150   }
 151   if (levelZero) {
 152     d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
 153   } else {
 154     d_typeMap->insert(name, make_pair(params, t));
 155   }
 156 }
 157
 158 bool SymbolTable::Implementation::isBoundType(const string& name) const
 159     throw() {
 160   return d_typeMap->find(name) != d_typeMap->end();
 161 }
 162
 163 Type SymbolTable::Implementation::lookupType(const string& name) const throw() {
 164   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 165   PrettyCheckArgument(p.first.size() == 0, name,
 166                       "type constructor arity is wrong: "
 167                       "`%s' requires %u parameters but was provided 0",
 168                       name.c_str(), p.first.size());
 169   return p.second;
 170 }
 171
 172 Type SymbolTable::Implementation::lookupType(const string& name,
 173                                              const vector<Type>& params) const
 174     throw() {
 175   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 176   PrettyCheckArgument(p.first.size() == params.size(), params,
 177                       "type constructor arity is wrong: "
 178                       "`%s' requires %u parameters but was provided %u",
 179                       name.c_str(), p.first.size(), params.size());
 180   if (p.first.size() == 0) {
 181     PrettyCheckArgument(p.second.isSort(), name.c_str());
 182     return p.second;
 183   }
 184   if (p.second.isSortConstructor()) {
 185     if (Debug.isOn("sort")) {
 186       Debug("sort") << "instantiating using a sort constructor" << endl;
 187       Debug("sort") << "have formals [";
 188       copy(p.first.begin(), p.first.end() - 1,
 189            ostream_iterator<Type>(Debug("sort"), ", "));
 190       Debug("sort") << p.first.back() << "]" << endl << "parameters   [";
 191       copy(params.begin(), params.end() - 1,
 192            ostream_iterator<Type>(Debug("sort"), ", "));
 193       Debug("sort") << params.back() << "]" << endl
 194                     << "type ctor    " << name << endl
 195                     << "type is      " << p.second << endl;
 196     }
 197
 198     Type instantiation = SortConstructorType(p.second).instantiate(params);
 199
 200     Debug("sort") << "instance is  " << instantiation << endl;
 201
 202     return instantiation;
 203   } else if (p.second.isDatatype()) {
 204     PrettyCheckArgument(DatatypeType(p.second).isParametric(), name,
 205                         "expected parametric datatype");
 206     return DatatypeType(p.second).instantiate(params);
 207   } else {
 208     if (Debug.isOn("sort")) {
 209       Debug("sort") << "instantiating using a sort substitution" << endl;
 210       Debug("sort") << "have formals [";
 211       copy(p.first.begin(), p.first.end() - 1,
 212            ostream_iterator<Type>(Debug("sort"), ", "));
 213       Debug("sort") << p.first.back() << "]" << endl << "parameters   [";
 214       copy(params.begin(), params.end() - 1,
 215            ostream_iterator<Type>(Debug("sort"), ", "));
 216       Debug("sort") << params.back() << "]" << endl
 217                     << "type ctor    " << name << endl
 218                     << "type is      " << p.second << endl;
 219     }
 220
 221     Type instantiation = p.second.substitute(p.first, params);
 222
 223     Debug("sort") << "instance is  " << instantiation << endl;
 224
 225     return instantiation;
 226   }
 227 }
 228
 229 size_t SymbolTable::Implementation::lookupArity(const string& name) {
 230   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 231   return p.first.size();
 232 }
 233
 234 void SymbolTable::Implementation::popScope() throw(ScopeException) {
 235   if (d_context.getLevel() == 0) {
 236     throw ScopeException();
 237   }
 238   d_context.pop();
 239 }
 240
 241 void SymbolTable::Implementation::pushScope() throw() { d_context.push(); }
 242
 243 size_t SymbolTable::Implementation::getLevel() const throw() {
 244   return d_context.getLevel();
 245 }
 246
 247 void SymbolTable::Implementation::reset() {
 248   this->SymbolTable::Implementation::~Implementation();
 249   new (this) SymbolTable::Implementation();
 250 }
 251
 252 SymbolTable::SymbolTable()
 253     : d_implementation(new SymbolTable::Implementation()) {}
 254
 255 SymbolTable::~SymbolTable() {}
 256
 257 void SymbolTable::bind(const string& name, Expr obj, bool levelZero) throw() {
 258   d_implementation->bind(name, obj, levelZero);
 259 }
 260
 261 void SymbolTable::bindDefinedFunction(const string& name, Expr obj,
 262                                       bool levelZero) throw() {
 263   d_implementation->bindDefinedFunction(name, obj, levelZero);
 264 }
 265
 266 void SymbolTable::bindType(const string& name, Type t, bool levelZero) throw() {
 267   d_implementation->bindType(name, t, levelZero);
 268 }
 269
 270 void SymbolTable::bindType(const string& name, const vector<Type>& params,
 271                            Type t, bool levelZero) throw() {
 272   d_implementation->bindType(name, params, t, levelZero);
 273 }
 274
 275 bool SymbolTable::isBound(const string& name) const throw() {
 276   return d_implementation->isBound(name);
 277 }
 278
 279 bool SymbolTable::isBoundDefinedFunction(const string& name) const throw() {
 280   return d_implementation->isBoundDefinedFunction(name);
 281 }
 282
 283 bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
 284   return d_implementation->isBoundDefinedFunction(func);
 285 }
 286 bool SymbolTable::isBoundType(const string& name) const throw() {
 287   return d_implementation->isBoundType(name);
 288 }
 289 Expr SymbolTable::lookup(const string& name) const throw() {
 290   return d_implementation->lookup(name);
 291 }
 292 Type SymbolTable::lookupType(const string& name) const throw() {
 293   return d_implementation->lookupType(name);
 294 }
 295
 296 Type SymbolTable::lookupType(const string& name,
 297                              const vector<Type>& params) const throw() {
 298   return d_implementation->lookupType(name, params);
 299 }
 300 size_t SymbolTable::lookupArity(const string& name) {
 301   return d_implementation->lookupArity(name);
 302 }
 303 void SymbolTable::popScope() throw(ScopeException) {
 304   d_implementation->popScope();
 305 }
 306
 307 void SymbolTable::pushScope() throw() { d_implementation->pushScope(); }
 308 size_t SymbolTable::getLevel() const throw() {
 309   return d_implementation->getLevel();
 310 }
 311 void SymbolTable::reset() { d_implementation->reset(); }
 312
 313 }  // namespace CVC4