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 <unordered_map>
  24 #include <utility>
  25
  26 #include "context/cdhashmap.h"
  27 #include "context/cdhashset.h"
  28 #include "context/context.h"
  29 #include "expr/expr.h"
  30 #include "expr/expr_manager_scope.h"
  31 #include "expr/type.h"
  32
  33 namespace CVC4 {
  34
  35 using ::CVC4::context::CDHashMap;
  36 using ::CVC4::context::CDHashSet;
  37 using ::CVC4::context::Context;
  38 using ::std::copy;
  39 using ::std::endl;
  40 using ::std::ostream_iterator;
  41 using ::std::pair;
  42 using ::std::string;
  43 using ::std::vector;
  44
  45 /** Overloaded type trie.
  46  *
  47  * This data structure stores a trie of expressions with
  48  * the same name, and must be distinguished by their argument types.
  49  * It is context-dependent.
  50  *
  51  * Using the argument allowFunVariants,
  52  * it may either be configured to allow function variants or not,
  53  * where a function variant is function that expects the same
  54  * argument types as another.
  55  *
  56  * For example, the following definitions introduce function
  57  * variants for the symbol f:
  58  *
  59  * 1. (declare-fun f (Int) Int) and
  60  *    (declare-fun f (Int) Bool)
  61  *
  62  * 2. (declare-fun f (Int) Int) and
  63  *    (declare-fun f (Int) Int)
  64  *
  65  * 3. (declare-datatypes ((Tup 0)) ((f (data Int)))) and
  66  *    (declare-fun f (Int) Tup)
  67  *
  68  * 4. (declare-datatypes ((Tup 0)) ((mkTup (f Int)))) and
  69  *    (declare-fun f (Tup) Bool)
  70  *
  71  * If function variants is set to true, we allow function variants
  72  * but not function redefinition. In examples 2 and 3, f is
  73  * declared twice as a symbol of identical argument and range
  74  * types. We never accept these definitions. However, we do
  75  * allow examples 1 and 4 above when allowFunVariants is true.
  76  *
  77  * For 0-argument functions (constants), we always allow
  78  * function variants.  That is, we always accept these examples:
  79  *
  80  * 5.  (declare-fun c () Int)
  81  *     (declare-fun c () Bool)
  82  *
  83  * 6.  (declare-datatypes ((Enum 0)) ((c)))
  84  *     (declare-fun c () Int)
  85  *
  86  * and always reject constant redefinition such as:
  87  *
  88  * 7. (declare-fun c () Int)
  89  *    (declare-fun c () Int)
  90  *
  91  * 8. (declare-datatypes ((Enum 0)) ((c))) and
  92  *    (declare-fun c () Enum)
  93  */
  94 class OverloadedTypeTrie {
  95  public:
  96   OverloadedTypeTrie(Context* c, bool allowFunVariants = false)
  97       : d_overloaded_symbols(new (true) CDHashSet<Expr, ExprHashFunction>(c)),
  98         d_allowFunctionVariants(allowFunVariants)
  99   {
 100   }
 101   ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
 102
 103   /** is this function overloaded? */
 104   bool isOverloadedFunction(Expr fun) const;
 105
 106   /** Get overloaded constant for type.
 107    * If possible, it returns a defined symbol with name
 108    * that has type t. Otherwise returns null expression.
 109    */
 110   Expr getOverloadedConstantForType(const std::string& name, Type t) const;
 111
 112   /**
 113    * If possible, returns a defined function for a name
 114    * and a vector of expected argument types. Otherwise returns
 115    * null expression.
 116    */
 117   Expr getOverloadedFunctionForTypes(const std::string& name,
 118                                      const std::vector<Type>& argTypes) const;
 119   /** called when obj is bound to name, and prev_bound_obj was already bound to
 120    * name Returns false if the binding is invalid.
 121    */
 122   bool bind(const string& name, Expr prev_bound_obj, Expr obj);
 123
 124  private:
 125   /** Marks expression obj with name as overloaded.
 126    * Adds relevant information to the type arg trie data structure.
 127    * It returns false if there is already an expression bound to that name
 128    * whose type expects the same arguments as the type of obj but is not
 129    * identical to the type of obj.  For example, if we declare :
 130    *
 131    * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
 132    * (declare-fun cons (Int List) List)
 133    *
 134    * cons : constructor_type( Int, List, List )
 135    * cons : function_type( Int, List, List )
 136    *
 137    * These are put in the same place in the trie but do not have identical type,
 138    * hence we return false.
 139    */
 140   bool markOverloaded(const string& name, Expr obj);
 141   /** the null expression */
 142   Expr d_nullExpr;
 143   // The (context-independent) trie storing that maps expected argument
 144   // vectors to symbols. All expressions stored in d_symbols are only
 145   // interpreted as active if they also appear in the context-dependent
 146   // set d_overloaded_symbols.
 147   class TypeArgTrie {
 148    public:
 149     // children of this node
 150     std::map<Type, TypeArgTrie> d_children;
 151     // symbols at this node
 152     std::map<Type, Expr> d_symbols;
 153   };
 154   /** for each string with operator overloading, this stores the data structure
 155    * above. */
 156   std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
 157   /** The set of overloaded symbols. */
 158   CDHashSet<Expr, ExprHashFunction>* d_overloaded_symbols;
 159   /** allow function variants
 160    * This is true if we allow overloading (non-constant) functions that expect
 161    * the same argument types.
 162    */
 163   bool d_allowFunctionVariants;
 164   /** get unique overloaded function
 165   * If tat->d_symbols contains an active overloaded function, it
 166   * returns that function, where that function must be unique
 167   * if reqUnique=true.
 168   * Otherwise, it returns the null expression.
 169   */
 170   Expr getOverloadedFunctionAt(const TypeArgTrie* tat, bool reqUnique=true) const;
 171 };
 172
 173 bool OverloadedTypeTrie::isOverloadedFunction(Expr fun) const {
 174   return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
 175 }
 176
 177 Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name,
 178                                                       Type t) const {
 179   std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
 180       d_overload_type_arg_trie.find(name);
 181   if (it != d_overload_type_arg_trie.end()) {
 182     std::map<Type, Expr>::const_iterator its = it->second.d_symbols.find(t);
 183     if (its != it->second.d_symbols.end()) {
 184       Expr expr = its->second;
 185       // must be an active symbol
 186       if (isOverloadedFunction(expr)) {
 187         return expr;
 188       }
 189     }
 190   }
 191   return d_nullExpr;
 192 }
 193
 194 Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
 195     const std::string& name, const std::vector<Type>& argTypes) const {
 196   std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
 197       d_overload_type_arg_trie.find(name);
 198   if (it != d_overload_type_arg_trie.end()) {
 199     const TypeArgTrie* tat = &it->second;
 200     for (unsigned i = 0; i < argTypes.size(); i++) {
 201       std::map<Type, TypeArgTrie>::const_iterator itc =
 202           tat->d_children.find(argTypes[i]);
 203       if (itc != tat->d_children.end()) {
 204         tat = &itc->second;
 205       } else {
 206         // no functions match
 207         return d_nullExpr;
 208       }
 209     }
 210     // we ensure that there is *only* one active symbol at this node
 211     return getOverloadedFunctionAt(tat);
 212   }
 213   return d_nullExpr;
 214 }
 215
 216 bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj,
 217                               Expr obj) {
 218   bool retprev = true;
 219   if (!isOverloadedFunction(prev_bound_obj)) {
 220     // mark previous as overloaded
 221     retprev = markOverloaded(name, prev_bound_obj);
 222   }
 223   // mark this as overloaded
 224   bool retobj = markOverloaded(name, obj);
 225   return retprev && retobj;
 226 }
 227
 228 bool OverloadedTypeTrie::markOverloaded(const string& name, Expr obj) {
 229   Trace("parser-overloading") << "Overloaded function : " << name;
 230   Trace("parser-overloading") << " with type " << obj.getType() << std::endl;
 231   // get the argument types
 232   Type t = obj.getType();
 233   Type rangeType = t;
 234   std::vector<Type> argTypes;
 235   if (t.isFunction()) {
 236     argTypes = static_cast<FunctionType>(t).getArgTypes();
 237     rangeType = static_cast<FunctionType>(t).getRangeType();
 238   } else if (t.isConstructor()) {
 239     argTypes = static_cast<ConstructorType>(t).getArgTypes();
 240     rangeType = static_cast<ConstructorType>(t).getRangeType();
 241   } else if (t.isTester()) {
 242     argTypes.push_back(static_cast<TesterType>(t).getDomain());
 243     rangeType = static_cast<TesterType>(t).getRangeType();
 244   } else if (t.isSelector()) {
 245     argTypes.push_back(static_cast<SelectorType>(t).getDomain());
 246     rangeType = static_cast<SelectorType>(t).getRangeType();
 247   }
 248   // add to the trie
 249   TypeArgTrie* tat = &d_overload_type_arg_trie[name];
 250   for (unsigned i = 0; i < argTypes.size(); i++) {
 251     tat = &(tat->d_children[argTypes[i]]);
 252   }
 253
 254   // check if function variants are allowed here
 255   if (d_allowFunctionVariants || argTypes.empty())
 256   {
 257     // they are allowed, check for redefinition
 258     std::map<Type, Expr>::iterator it = tat->d_symbols.find(rangeType);
 259     if (it != tat->d_symbols.end())
 260     {
 261       Expr prev_obj = it->second;
 262       // if there is already an active function with the same name and expects
 263       // the same argument types and has the same return type, we reject the
 264       // re-declaration here.
 265       if (isOverloadedFunction(prev_obj))
 266       {
 267         return false;
 268       }
 269     }
 270   }
 271   else
 272   {
 273     // they are not allowed, we cannot have any function defined here.
 274     Expr existingFun = getOverloadedFunctionAt(tat, false);
 275     if (!existingFun.isNull())
 276     {
 277       return false;
 278     }
 279   }
 280
 281   // otherwise, update the symbols
 282   d_overloaded_symbols->insert(obj);
 283   tat->d_symbols[rangeType] = obj;
 284   return true;
 285 }
 286
 287 Expr OverloadedTypeTrie::getOverloadedFunctionAt(
 288     const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const
 289 {
 290   Expr retExpr;
 291   for (std::map<Type, Expr>::const_iterator its = tat->d_symbols.begin();
 292        its != tat->d_symbols.end();
 293        ++its)
 294   {
 295     Expr expr = its->second;
 296     if (isOverloadedFunction(expr))
 297     {
 298       if (retExpr.isNull())
 299       {
 300         if (!reqUnique)
 301         {
 302           return expr;
 303         }
 304         else
 305         {
 306           retExpr = expr;
 307         }
 308       }
 309       else
 310       {
 311         // multiple functions match
 312         return d_nullExpr;
 313       }
 314     }
 315   }
 316   return retExpr;
 317 }
 318
 319 class SymbolTable::Implementation {
 320  public:
 321   Implementation()
 322       : d_context(),
 323         d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
 324         d_typeMap(new (true) TypeMap(&d_context)),
 325         d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {
 326     d_overload_trie = new OverloadedTypeTrie(&d_context);
 327   }
 328
 329   ~Implementation() {
 330     d_exprMap->deleteSelf();
 331     d_typeMap->deleteSelf();
 332     d_functions->deleteSelf();
 333     delete d_overload_trie;
 334   }
 335
 336   bool bind(const string& name, Expr obj, bool levelZero, bool doOverload);
 337   bool bindDefinedFunction(const string& name, Expr obj, bool levelZero,
 338                            bool doOverload);
 339   void bindType(const string& name, Type t, bool levelZero = false);
 340   void bindType(const string& name, const vector<Type>& params, Type t,
 341                 bool levelZero = false);
 342   bool isBound(const string& name) const;
 343   bool isBoundDefinedFunction(const string& name) const;
 344   bool isBoundDefinedFunction(Expr func) const;
 345   bool isBoundType(const string& name) const;
 346   Expr lookup(const string& name) const;
 347   Type lookupType(const string& name) const;
 348   Type lookupType(const string& name, const vector<Type>& params) const;
 349   size_t lookupArity(const string& name);
 350   void popScope();
 351   void pushScope();
 352   size_t getLevel() const;
 353   void reset();
 354   //------------------------ operator overloading
 355   /** implementation of function from header */
 356   bool isOverloadedFunction(Expr fun) const;
 357
 358   /** implementation of function from header */
 359   Expr getOverloadedConstantForType(const std::string& name, Type t) const;
 360
 361   /** implementation of function from header */
 362   Expr getOverloadedFunctionForTypes(const std::string& name,
 363                                      const std::vector<Type>& argTypes) const;
 364   //------------------------ end operator overloading
 365  private:
 366   /** The context manager for the scope maps. */
 367   Context d_context;
 368
 369   /** A map for expressions. */
 370   CDHashMap<string, Expr>* d_exprMap;
 371
 372   /** A map for types. */
 373   using TypeMap = CDHashMap<string, std::pair<vector<Type>, Type>>;
 374   TypeMap* d_typeMap;
 375
 376   /** A set of defined functions. */
 377   CDHashSet<Expr, ExprHashFunction>* d_functions;
 378
 379   //------------------------ operator overloading
 380   // the null expression
 381   Expr d_nullExpr;
 382   // overloaded type trie, stores all information regarding overloading
 383   OverloadedTypeTrie* d_overload_trie;
 384   /** bind with overloading
 385    * This is called whenever obj is bound to name where overloading symbols is
 386    * allowed. If a symbol is previously bound to that name, it marks both as
 387    * overloaded. Returns false if the binding was invalid.
 388    */
 389   bool bindWithOverloading(const string& name, Expr obj);
 390   //------------------------ end operator overloading
 391 }; /* SymbolTable::Implementation */
 392
 393 bool SymbolTable::Implementation::bind(const string& name, Expr obj,
 394                                        bool levelZero, bool doOverload) {
 395   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
 396   ExprManagerScope ems(obj);
 397   if (doOverload) {
 398     if (!bindWithOverloading(name, obj)) {
 399       return false;
 400     }
 401   }
 402   if (levelZero) {
 403     d_exprMap->insertAtContextLevelZero(name, obj);
 404   } else {
 405     d_exprMap->insert(name, obj);
 406   }
 407   return true;
 408 }
 409
 410 bool SymbolTable::Implementation::bindDefinedFunction(const string& name,
 411                                                       Expr obj, bool levelZero,
 412                                                       bool doOverload) {
 413   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
 414   ExprManagerScope ems(obj);
 415   if (doOverload) {
 416     if (!bindWithOverloading(name, obj)) {
 417       return false;
 418     }
 419   }
 420   if (levelZero) {
 421     d_exprMap->insertAtContextLevelZero(name, obj);
 422     d_functions->insertAtContextLevelZero(obj);
 423   } else {
 424     d_exprMap->insert(name, obj);
 425     d_functions->insert(obj);
 426   }
 427   return true;
 428 }
 429
 430 bool SymbolTable::Implementation::isBound(const string& name) const {
 431   return d_exprMap->find(name) != d_exprMap->end();
 432 }
 433
 434 bool SymbolTable::Implementation::isBoundDefinedFunction(
 435     const string& name) const {
 436   CDHashMap<string, Expr>::iterator found = d_exprMap->find(name);
 437   return found != d_exprMap->end() && d_functions->contains((*found).second);
 438 }
 439
 440 bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const {
 441   return d_functions->contains(func);
 442 }
 443
 444 Expr SymbolTable::Implementation::lookup(const string& name) const {
 445   Assert(isBound(name));
 446   Expr expr = (*d_exprMap->find(name)).second;
 447   if (isOverloadedFunction(expr)) {
 448     return d_nullExpr;
 449   } else {
 450     return expr;
 451   }
 452 }
 453
 454 void SymbolTable::Implementation::bindType(const string& name, Type t,
 455                                            bool levelZero) {
 456   if (levelZero) {
 457     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
 458   } else {
 459     d_typeMap->insert(name, make_pair(vector<Type>(), t));
 460   }
 461 }
 462
 463 void SymbolTable::Implementation::bindType(const string& name,
 464                                            const vector<Type>& params, Type t,
 465                                            bool levelZero) {
 466   if (Debug.isOn("sort")) {
 467     Debug("sort") << "bindType(" << name << ", [";
 468     if (params.size() > 0) {
 469       copy(params.begin(), params.end() - 1,
 470            ostream_iterator<Type>(Debug("sort"), ", "));
 471       Debug("sort") << params.back();
 472     }
 473     Debug("sort") << "], " << t << ")" << endl;
 474   }
 475   if (levelZero) {
 476     d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
 477   } else {
 478     d_typeMap->insert(name, make_pair(params, t));
 479   }
 480 }
 481
 482 bool SymbolTable::Implementation::isBoundType(const string& name) const {
 483   return d_typeMap->find(name) != d_typeMap->end();
 484 }
 485
 486 Type SymbolTable::Implementation::lookupType(const string& name) const {
 487   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 488   PrettyCheckArgument(p.first.size() == 0, name,
 489                       "type constructor arity is wrong: "
 490                       "`%s' requires %u parameters but was provided 0",
 491                       name.c_str(), p.first.size());
 492   return p.second;
 493 }
 494
 495 Type SymbolTable::Implementation::lookupType(const string& name,
 496                                              const vector<Type>& params) const {
 497   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 498   PrettyCheckArgument(p.first.size() == params.size(), params,
 499                       "type constructor arity is wrong: "
 500                       "`%s' requires %u parameters but was provided %u",
 501                       name.c_str(), p.first.size(), params.size());
 502   if (p.first.size() == 0) {
 503     PrettyCheckArgument(p.second.isSort(), name.c_str());
 504     return p.second;
 505   }
 506   if (p.second.isSortConstructor()) {
 507     if (Debug.isOn("sort")) {
 508       Debug("sort") << "instantiating using a sort constructor" << endl;
 509       Debug("sort") << "have formals [";
 510       copy(p.first.begin(), p.first.end() - 1,
 511            ostream_iterator<Type>(Debug("sort"), ", "));
 512       Debug("sort") << p.first.back() << "]" << endl << "parameters   [";
 513       copy(params.begin(), params.end() - 1,
 514            ostream_iterator<Type>(Debug("sort"), ", "));
 515       Debug("sort") << params.back() << "]" << endl
 516                     << "type ctor    " << name << endl
 517                     << "type is      " << p.second << endl;
 518     }
 519
 520     Type instantiation = SortConstructorType(p.second).instantiate(params);
 521
 522     Debug("sort") << "instance is  " << instantiation << endl;
 523
 524     return instantiation;
 525   } else if (p.second.isDatatype()) {
 526     PrettyCheckArgument(DatatypeType(p.second).isParametric(), name,
 527                         "expected parametric datatype");
 528     return DatatypeType(p.second).instantiate(params);
 529   } else {
 530     if (Debug.isOn("sort")) {
 531       Debug("sort") << "instantiating using a sort substitution" << endl;
 532       Debug("sort") << "have formals [";
 533       copy(p.first.begin(), p.first.end() - 1,
 534            ostream_iterator<Type>(Debug("sort"), ", "));
 535       Debug("sort") << p.first.back() << "]" << endl << "parameters   [";
 536       copy(params.begin(), params.end() - 1,
 537            ostream_iterator<Type>(Debug("sort"), ", "));
 538       Debug("sort") << params.back() << "]" << endl
 539                     << "type ctor    " << name << endl
 540                     << "type is      " << p.second << endl;
 541     }
 542
 543     Type instantiation = p.second.substitute(p.first, params);
 544
 545     Debug("sort") << "instance is  " << instantiation << endl;
 546
 547     return instantiation;
 548   }
 549 }
 550
 551 size_t SymbolTable::Implementation::lookupArity(const string& name) {
 552   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
 553   return p.first.size();
 554 }
 555
 556 void SymbolTable::Implementation::popScope() {
 557   if (d_context.getLevel() == 0) {
 558     throw ScopeException();
 559   }
 560   d_context.pop();
 561 }
 562
 563 void SymbolTable::Implementation::pushScope() { d_context.push(); }
 564
 565 size_t SymbolTable::Implementation::getLevel() const {
 566   return d_context.getLevel();
 567 }
 568
 569 void SymbolTable::Implementation::reset() {
 570   this->SymbolTable::Implementation::~Implementation();
 571   new (this) SymbolTable::Implementation();
 572 }
 573
 574 bool SymbolTable::Implementation::isOverloadedFunction(Expr fun) const {
 575   return d_overload_trie->isOverloadedFunction(fun);
 576 }
 577
 578 Expr SymbolTable::Implementation::getOverloadedConstantForType(
 579     const std::string& name, Type t) const {
 580   return d_overload_trie->getOverloadedConstantForType(name, t);
 581 }
 582
 583 Expr SymbolTable::Implementation::getOverloadedFunctionForTypes(
 584     const std::string& name, const std::vector<Type>& argTypes) const {
 585   return d_overload_trie->getOverloadedFunctionForTypes(name, argTypes);
 586 }
 587
 588 bool SymbolTable::Implementation::bindWithOverloading(const string& name,
 589                                                       Expr obj) {
 590   CDHashMap<string, Expr>::const_iterator it = d_exprMap->find(name);
 591   if (it != d_exprMap->end()) {
 592     const Expr& prev_bound_obj = (*it).second;
 593     if (prev_bound_obj != obj) {
 594       return d_overload_trie->bind(name, prev_bound_obj, obj);
 595     }
 596   }
 597   return true;
 598 }
 599
 600 bool SymbolTable::isOverloadedFunction(Expr fun) const {
 601   return d_implementation->isOverloadedFunction(fun);
 602 }
 603
 604 Expr SymbolTable::getOverloadedConstantForType(const std::string& name,
 605                                                Type t) const {
 606   return d_implementation->getOverloadedConstantForType(name, t);
 607 }
 608
 609 Expr SymbolTable::getOverloadedFunctionForTypes(
 610     const std::string& name, const std::vector<Type>& argTypes) const {
 611   return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
 612 }
 613
 614 SymbolTable::SymbolTable()
 615     : d_implementation(new SymbolTable::Implementation()) {}
 616
 617 SymbolTable::~SymbolTable() {}
 618 bool SymbolTable::bind(const string& name,
 619                        Expr obj,
 620                        bool levelZero,
 621                        bool doOverload)
 622 {
 623   return d_implementation->bind(name, obj, levelZero, doOverload);
 624 }
 625
 626 bool SymbolTable::bindDefinedFunction(const string& name,
 627                                       Expr obj,
 628                                       bool levelZero,
 629                                       bool doOverload)
 630 {
 631   return d_implementation->bindDefinedFunction(name, obj, levelZero,
 632                                                doOverload);
 633 }
 634
 635 void SymbolTable::bindType(const string& name, Type t, bool levelZero)
 636 {
 637   d_implementation->bindType(name, t, levelZero);
 638 }
 639
 640 void SymbolTable::bindType(const string& name,
 641                            const vector<Type>& params,
 642                            Type t,
 643                            bool levelZero)
 644 {
 645   d_implementation->bindType(name, params, t, levelZero);
 646 }
 647
 648 bool SymbolTable::isBound(const string& name) const
 649 {
 650   return d_implementation->isBound(name);
 651 }
 652
 653 bool SymbolTable::isBoundDefinedFunction(const string& name) const
 654 {
 655   return d_implementation->isBoundDefinedFunction(name);
 656 }
 657
 658 bool SymbolTable::isBoundDefinedFunction(Expr func) const
 659 {
 660   return d_implementation->isBoundDefinedFunction(func);
 661 }
 662 bool SymbolTable::isBoundType(const string& name) const
 663 {
 664   return d_implementation->isBoundType(name);
 665 }
 666 Expr SymbolTable::lookup(const string& name) const
 667 {
 668   return d_implementation->lookup(name);
 669 }
 670 Type SymbolTable::lookupType(const string& name) const
 671 {
 672   return d_implementation->lookupType(name);
 673 }
 674
 675 Type SymbolTable::lookupType(const string& name,
 676                              const vector<Type>& params) const
 677 {
 678   return d_implementation->lookupType(name, params);
 679 }
 680 size_t SymbolTable::lookupArity(const string& name) {
 681   return d_implementation->lookupArity(name);
 682 }
 683 void SymbolTable::popScope() { d_implementation->popScope(); }
 684 void SymbolTable::pushScope() { d_implementation->pushScope(); }
 685 size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); }
 686 void SymbolTable::reset() { d_implementation->reset(); }
 687
 688 }  // namespace CVC4