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, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 <string>
  22 #include <utility>
  23
  24 #include "context/cdhashmap.h"
  25 #include "context/cdhashset.h"
  26 #include "context/context.h"
  27 #include "expr/expr.h"
  28 #include "expr/expr_manager_scope.h"
  29 #include "expr/type.h"
  30
  31
  32 using namespace CVC4::context;
  33 using namespace std;
  34
  35 namespace CVC4 {
  36
  37 SymbolTable::SymbolTable() :
  38   d_context(new Context()),
  39   d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
  40   d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
  41   d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
  42 }
  43
  44 SymbolTable::~SymbolTable() {
  45   d_exprMap->deleteSelf();
  46   d_typeMap->deleteSelf();
  47   d_functions->deleteSelf();
  48   delete d_context;
  49 }
  50
  51 void SymbolTable::bind(const std::string& name, Expr obj,
  52                        bool levelZero) throw() {
  53   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
  54   ExprManagerScope ems(obj);
  55   if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
  56   else d_exprMap->insert(name, obj);
  57 }
  58
  59 void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
  60                                       bool levelZero) throw() {
  61   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
  62   ExprManagerScope ems(obj);
  63   if(levelZero){
  64     d_exprMap->insertAtContextLevelZero(name, obj);
  65     d_functions->insertAtContextLevelZero(obj);
  66   } else {
  67     d_exprMap->insert(name, obj);
  68     d_functions->insert(obj);
  69   }
  70 }
  71
  72 bool SymbolTable::isBound(const std::string& name) const throw() {
  73   return d_exprMap->find(name) != d_exprMap->end();
  74 }
  75
  76 bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() {
  77   CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
  78     d_exprMap->find(name);
  79   return found != d_exprMap->end() && d_functions->contains((*found).second);
  80 }
  81
  82 bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
  83   return d_functions->contains(func);
  84 }
  85
  86 Expr SymbolTable::lookup(const std::string& name) const throw() {
  87   return (*d_exprMap->find(name)).second;
  88 }
  89
  90 void SymbolTable::bindType(const std::string& name, Type t,
  91                            bool levelZero) throw() {
  92   if(levelZero) {
  93     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
  94   } else {
  95     d_typeMap->insert(name, make_pair(vector<Type>(), t));
  96   }
  97 }
  98
  99 void SymbolTable::bindType(const std::string& name,
 100                            const std::vector<Type>& params,
 101                            Type t,
 102                            bool levelZero) throw() {
 103   if(Debug.isOn("sort")) {
 104     Debug("sort") << "bindType(" << name << ", [";
 105     if(params.size() > 0) {
 106       copy( params.begin(), params.end() - 1,
 107             ostream_iterator<Type>(Debug("sort"), ", ") );
 108       Debug("sort") << params.back();
 109     }
 110     Debug("sort") << "], " << t << ")" << endl;
 111   }
 112   if(levelZero) {
 113     d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
 114   } else {
 115     d_typeMap->insert(name, make_pair(params, t));
 116   }
 117 }
 118
 119 bool SymbolTable::isBoundType(const std::string& name) const throw() {
 120   return d_typeMap->find(name) != d_typeMap->end();
 121 }
 122
 123 Type SymbolTable::lookupType(const std::string& name) const throw() {
 124   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 125   PrettyCheckArgument(p.first.size() == 0, name,
 126                 "type constructor arity is wrong: "
 127                 "`%s' requires %u parameters but was provided 0",
 128                 name.c_str(), p.first.size());
 129   return p.second;
 130 }
 131
 132 Type SymbolTable::lookupType(const std::string& name,
 133                              const std::vector<Type>& params) const throw() {
 134   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 135   PrettyCheckArgument(p.first.size() == params.size(), params,
 136                 "type constructor arity is wrong: "
 137                 "`%s' requires %u parameters but was provided %u",
 138          name.c_str(), p.first.size(), params.size());
 139   if(p.first.size() == 0) {
 140     PrettyCheckArgument(p.second.isSort(), name.c_str());
 141     return p.second;
 142   }
 143   if(p.second.isSortConstructor()) {
 144     if(Debug.isOn("sort")) {
 145       Debug("sort") << "instantiating using a sort constructor" << endl;
 146       Debug("sort") << "have formals [";
 147       copy( p.first.begin(), p.first.end() - 1,
 148             ostream_iterator<Type>(Debug("sort"), ", ") );
 149       Debug("sort") << p.first.back() << "]" << endl
 150                     << "parameters   [";
 151       copy( params.begin(), params.end() - 1,
 152             ostream_iterator<Type>(Debug("sort"), ", ") );
 153       Debug("sort") << params.back() << "]" << endl
 154                     << "type ctor    " << name << endl
 155                     << "type is      " << p.second << endl;
 156     }
 157
 158     Type instantiation =
 159       SortConstructorType(p.second).instantiate(params);
 160
 161     Debug("sort") << "instance is  " << instantiation << endl;
 162
 163     return instantiation;
 164   } else if(p.second.isDatatype()) {
 165     PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
 166     return DatatypeType(p.second).instantiate(params);
 167   } else {
 168     if(Debug.isOn("sort")) {
 169       Debug("sort") << "instantiating using a sort substitution" << endl;
 170       Debug("sort") << "have formals [";
 171       copy( p.first.begin(), p.first.end() - 1,
 172             ostream_iterator<Type>(Debug("sort"), ", ") );
 173       Debug("sort") << p.first.back() << "]" << endl
 174                     << "parameters   [";
 175       copy( params.begin(), params.end() - 1,
 176             ostream_iterator<Type>(Debug("sort"), ", ") );
 177       Debug("sort") << params.back() << "]" << endl
 178                     << "type ctor    " << name << endl
 179                     << "type is      " << p.second << endl;
 180     }
 181
 182     Type instantiation = p.second.substitute(p.first, params);
 183
 184     Debug("sort") << "instance is  " << instantiation << endl;
 185
 186     return instantiation;
 187   }
 188 }
 189
 190 size_t SymbolTable::lookupArity(const std::string& name) {
 191   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 192   return p.first.size();
 193 }
 194
 195 void SymbolTable::popScope() throw(ScopeException) {
 196   if( d_context->getLevel() == 0 ) {
 197     throw ScopeException();
 198   }
 199   d_context->pop();
 200 }
 201
 202 void SymbolTable::pushScope() throw() {
 203   d_context->push();
 204 }
 205
 206 size_t SymbolTable::getLevel() const throw() {
 207   return d_context->getLevel();
 208 }
 209
 210 void SymbolTable::reset() {
 211   this->SymbolTable::~SymbolTable();
 212   new(this) SymbolTable();
 213 }
 214
 215 }/* CVC4 namespace */