src/expr/symbol_table.cpp

   1 /*********************                                                        */
   2 /*! \file symbol_table.cpp
   3  ** \verbatim
   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
  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 #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"
  26
  27 #include <string>
  28 #include <utility>
  29
  30 using namespace CVC4;
  31 using namespace CVC4::context;
  32 using namespace std;
  33
  34 namespace CVC4 {
  35
  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)) {
  41 }
  42
  43 SymbolTable::~SymbolTable() {
  44   d_exprMap->deleteSelf();
  45   d_typeMap->deleteSelf();
  46   d_functions->deleteSelf();
  47   delete d_context;
  48 }
  49
  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);
  56 }
  57
  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);
  62   if(levelZero){
  63     d_exprMap->insertAtContextLevelZero(name, obj);
  64     d_functions->insertAtContextLevelZero(obj);
  65   } else {
  66     d_exprMap->insert(name, obj);
  67     d_functions->insert(obj);
  68   }
  69 }
  70
  71 bool SymbolTable::isBound(const std::string& name) const throw() {
  72   return d_exprMap->find(name) != d_exprMap->end();
  73 }
  74
  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);
  79 }
  80
  81 bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
  82   return d_functions->contains(func);
  83 }
  84
  85 Expr SymbolTable::lookup(const std::string& name) const throw() {
  86   return (*d_exprMap->find(name)).second;
  87 }
  88
  89 void SymbolTable::bindType(const std::string& name, Type t,
  90                            bool levelZero) throw() {
  91   if(levelZero) {
  92     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
  93   } else {
  94     d_typeMap->insert(name, make_pair(vector<Type>(), t));
  95   }
  96 }
  97
  98 void SymbolTable::bindType(const std::string& name,
  99                            const std::vector<Type>& params,
 100                            Type t,
 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();
 108     }
 109     Debug("sort") << "], " << t << ")" << endl;
 110   }
 111   if(levelZero) {
 112     d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
 113   } else {
 114     d_typeMap->insert(name, make_pair(params, t));
 115   }
 116 }
 117
 118 bool SymbolTable::isBoundType(const std::string& name) const throw() {
 119   return d_typeMap->find(name) != d_typeMap->end();
 120 }
 121
 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());
 128   return p.second;
 129 }
 130
 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);
 140     return p.second;
 141   }
 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
 149                     << "parameters   [";
 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;
 155     }
 156
 157     Type instantiation =
 158       SortConstructorType(p.second).instantiate(params);
 159
 160     Debug("sort") << "instance is  " << instantiation << endl;
 161
 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);
 166   } else {
 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
 173                     << "parameters   [";
 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;
 179     }
 180
 181     Type instantiation = p.second.substitute(p.first, params);
 182
 183     Debug("sort") << "instance is  " << instantiation << endl;
 184
 185     return instantiation;
 186   }
 187 }
 188
 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();
 192 }
 193
 194 void SymbolTable::popScope() throw(ScopeException) {
 195   if( d_context->getLevel() == 0 ) {
 196     throw ScopeException();
 197   }
 198   d_context->pop();
 199 }
 200
 201 void SymbolTable::pushScope() throw() {
 202   d_context->push();
 203 }
 204
 205 size_t SymbolTable::getLevel() const throw() {
 206   return d_context->getLevel();
 207 }
 208
 209 void SymbolTable::reset() {
 210   this->SymbolTable::~SymbolTable();
 211   new(this) SymbolTable();
 212 }
 213
 214 }/* CVC4 namespace */