src/expr/symbol_table.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Morgan Deters, Christopher L. Conway
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Convenience class for scoping variable and type declarations.
  14  */
  15
  16 #include "cvc5_public.h"
  17
  18 #ifndef CVC5__SYMBOL_TABLE_H
  19 #define CVC5__SYMBOL_TABLE_H
  20
  21 #include <memory>
  22 #include <string>
  23 #include <vector>
  24
  25 #include "base/exception.h"
  26 #include "cvc5_export.h"
  27
  28 namespace cvc5 {
  29
  30 namespace api {
  31 class Solver;
  32 class Sort;
  33 class Term;
  34 }  // namespace api
  35
  36 class CVC5_EXPORT ScopeException : public Exception
  37 {
  38 };
  39
  40 /**
  41  * A convenience class for handling scoped declarations. Implements the usual
  42  * nested scoping rules for declarations, with separate bindings for expressions
  43  * and types.
  44  */
  45 class CVC5_EXPORT SymbolTable
  46 {
  47  public:
  48   /** Create a symbol table. */
  49   SymbolTable();
  50   ~SymbolTable();
  51
  52   /**
  53    * Bind an expression to a name in the current scope level.
  54    *
  55    * When doOverload is false:
  56    * if <code>name</code> is already bound to an expression in the current
  57    * level, then the binding is replaced. If <code>name</code> is bound
  58    * in a previous level, then the binding is "covered" by this one
  59    * until the current scope is popped.
  60    * If levelZero is true the name shouldn't be already bound.
  61    *
  62    * When doOverload is true:
  63    * if <code>name</code> is already bound to an expression in the current
  64    * level, then we mark the previous bound expression and obj as overloaded
  65    * functions.
  66    *
  67    * @param name an identifier
  68    * @param obj the expression to bind to <code>name</code>
  69    * @param levelZero set if the binding must be done at level 0
  70    * @param doOverload set if the binding can overload the function name.
  71    *
  72    * Returns false if the binding was invalid.
  73    */
  74   bool bind(const std::string& name,
  75             api::Term obj,
  76             bool levelZero = false,
  77             bool doOverload = false);
  78
  79   /**
  80    * Bind a type to a name in the current scope.  If <code>name</code>
  81    * is already bound to a type in the current level, then the binding
  82    * is replaced. If <code>name</code> is bound in a previous level,
  83    * then the binding is "covered" by this one until the current scope
  84    * is popped.
  85    *
  86    * @param name an identifier
  87    * @param t the type to bind to <code>name</code>
  88    * @param levelZero set if the binding must be done at level 0
  89    */
  90   void bindType(const std::string& name, api::Sort t, bool levelZero = false);
  91
  92   /**
  93    * Bind a type to a name in the current scope.  If <code>name</code>
  94    * is already bound to a type or type constructor in the current
  95    * level, then the binding is replaced. If <code>name</code> is
  96    * bound in a previous level, then the binding is "covered" by this
  97    * one until the current scope is popped.
  98    *
  99    * @param name an identifier
 100    * @param params the parameters to the type
 101    * @param t the type to bind to <code>name</code>
 102    * @param levelZero true to bind it globally (default is to bind it
 103    * locally within the current scope)
 104    */
 105   void bindType(const std::string& name,
 106                 const std::vector<api::Sort>& params,
 107                 api::Sort t,
 108                 bool levelZero = false);
 109
 110   /**
 111    * Check whether a name is bound to an expression with bind().
 112    *
 113    * @param name the identifier to check.
 114    * @returns true iff name is bound in the current scope.
 115    */
 116   bool isBound(const std::string& name) const;
 117
 118   /**
 119    * Check whether a name is bound to a type (or type constructor).
 120    *
 121    * @param name the identifier to check.
 122    * @returns true iff name is bound to a type in the current scope.
 123    */
 124   bool isBoundType(const std::string& name) const;
 125
 126   /**
 127    * Lookup a bound expression.
 128    *
 129    * @param name the identifier to lookup
 130    * @returns the unique expression bound to <code>name</code> in the current
 131    * scope.
 132    * It returns the null expression if there is not a unique expression bound to
 133    * <code>name</code> in the current scope (i.e. if there is not exactly one).
 134    */
 135   api::Term lookup(const std::string& name) const;
 136
 137   /**
 138    * Lookup a bound type.
 139    *
 140    * @param name the type identifier to lookup
 141    * @returns the type bound to <code>name</code> in the current scope.
 142    */
 143   api::Sort lookupType(const std::string& name) const;
 144
 145   /**
 146    * Lookup a bound parameterized type.
 147    *
 148    * @param name the type-constructor identifier to lookup
 149    * @param params the types to use to parameterize the type
 150    * @returns the type bound to <code>name(<i>params</i>)</code> in
 151    * the current scope.
 152    */
 153   api::Sort lookupType(const std::string& name,
 154                        const std::vector<api::Sort>& params) const;
 155
 156   /**
 157    * Lookup the arity of a bound parameterized type.
 158    */
 159   size_t lookupArity(const std::string& name);
 160
 161   /**
 162    * Pop a scope level, deletes all bindings since the last call to pushScope,
 163    * and decreases the level by 1.
 164    *
 165    * @throws ScopeException if the scope level is 0.
 166    */
 167   void popScope();
 168
 169   /** Push a scope level and increase the scope level by 1. */
 170   void pushScope();
 171
 172   /** Get the current level of this symbol table. */
 173   size_t getLevel() const;
 174
 175   /** Reset everything. */
 176   void reset();
 177   /** Reset assertions. */
 178   void resetAssertions();
 179
 180   //------------------------ operator overloading
 181   /** is this function overloaded? */
 182   bool isOverloadedFunction(api::Term fun) const;
 183
 184   /** Get overloaded constant for type.
 185    * If possible, it returns the defined symbol with name
 186    * that has type t. Otherwise returns null expression.
 187   */
 188   api::Term getOverloadedConstantForType(const std::string& name,
 189                                          api::Sort t) const;
 190
 191   /**
 192    * If possible, returns the unique defined function for a name
 193    * that expects arguments with types "argTypes".
 194    * For example, if argTypes = (T1, ..., Tn), then this may return an
 195    * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
 196    *
 197    * If there is not a unique defined function for the name and argTypes,
 198    * this returns the null expression. This can happen either if there are
 199    * no functions with name and expected argTypes, or alternatively there is
 200    * more than one function with name and expected argTypes.
 201    */
 202   api::Term getOverloadedFunctionForTypes(
 203       const std::string& name, const std::vector<api::Sort>& argTypes) const;
 204   //------------------------ end operator overloading
 205
 206  private:
 207   /** The implementation of the symbol table */
 208   class Implementation;
 209   std::unique_ptr<Implementation> d_implementation;
 210 }; /* class SymbolTable */
 211
 212 }  // namespace cvc5
 213
 214 #endif /* CVC5__SYMBOL_TABLE_H */