src/expr/variable_type_map.h

   1 /*********************                                                        */
   2 /*! \file variable_type_map.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Paul Meng
   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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_public.h"
  19
  20 #ifndef __CVC4__VARIABLE_TYPE_MAP_H
  21 #define __CVC4__VARIABLE_TYPE_MAP_H
  22
  23 #include <unordered_map>
  24
  25 #include "expr/expr.h"
  26
  27 namespace CVC4 {
  28
  29 class Expr;
  30 struct ExprHashFunction;
  31 class Type;
  32 struct TypeHashFunction;
  33
  34 class CVC4_PUBLIC VariableTypeMap {
  35   /**
  36    * A map Expr -> Expr, intended to be used for a mapping of variables
  37    * between two ExprManagers.
  38    */
  39   std::unordered_map<Expr, Expr, ExprHashFunction> d_variables;
  40
  41   /**
  42    * A map Type -> Type, intended to be used for a mapping of types
  43    * between two ExprManagers.
  44    */
  45   std::unordered_map<Type, Type, TypeHashFunction> d_types;
  46
  47 public:
  48   Expr& operator[](Expr e) { return d_variables[e]; }
  49   Type& operator[](Type t) { return d_types[t]; }
  50
  51 };/* class VariableTypeMap */
  52
  53 typedef std::unordered_map<uint64_t, uint64_t> VarMap;
  54
  55 struct CVC4_PUBLIC ExprManagerMapCollection {
  56   VariableTypeMap d_typeMap;
  57   VarMap d_to;
  58   VarMap d_from;
  59 };/* struct ExprManagerMapCollection */
  60
  61 }/* CVC4 namespace */
  62
  63 #endif /* __CVC4__VARIABLE_MAP_H */