src/theory/arith/arithvar_node_map.h

   1 /*********************                                                        */
   2 /*! \file arithvar_node_map.h
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
  21 #define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
  22
  23
  24 #include "theory/arith/arithvar.h"
  25 #include "context/context.h"
  26 #include "context/cdlist.h"
  27 #include "context/cdhashmap.h"
  28 #include "context/cdo.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace arith {
  33
  34 class ArithVarNodeMap {
  35 private:
  36   /**
  37    * Bidirectional map between Nodes and ArithVars.
  38    */
  39   NodeToArithVarMap d_nodeToArithVarMap;
  40   ArithVarToNodeMap d_arithVarToNodeMap;
  41
  42 public:
  43
  44   typedef ArithVarToNodeMap::const_iterator var_iterator;
  45
  46   ArithVarNodeMap() {}
  47
  48   inline bool hasArithVar(TNode x) const {
  49     return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
  50   }
  51
  52   inline bool hasNode(ArithVar a) const {
  53     return d_arithVarToNodeMap.isKey(a);
  54   }
  55
  56   inline ArithVar asArithVar(TNode x) const{
  57     Assert(hasArithVar(x));
  58     Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
  59     return (d_nodeToArithVarMap.find(x))->second;
  60   }
  61
  62   inline Node asNode(ArithVar a) const{
  63     Assert(hasNode(a));
  64     return d_arithVarToNodeMap[a];
  65   }
  66
  67   inline void setArithVar(TNode x, ArithVar a){
  68     Assert(!hasArithVar(x));
  69     Assert(!d_arithVarToNodeMap.isKey(a));
  70     d_arithVarToNodeMap.set(a, x);
  71     d_nodeToArithVarMap[x] = a;
  72   }
  73
  74   inline void remove(ArithVar x){
  75     Assert(hasNode(x));
  76     Node node = asNode(x);
  77
  78     d_nodeToArithVarMap.erase(d_nodeToArithVarMap.find(node));
  79     d_arithVarToNodeMap.remove(x);
  80   }
  81
  82   var_iterator var_begin() const {
  83     return d_arithVarToNodeMap.begin();
  84   }
  85   var_iterator var_end() const {
  86     return d_arithVarToNodeMap.end();
  87   }
  88
  89 };/* class ArithVarNodeMap */
  90
  91 }/* CVC4::theory::arith namespace */
  92 }/* CVC4::theory namespace */
  93 }/* CVC4 namespace */
  94
  95 #endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */