1 /********************* */
2 /*! \file arithvar_node_map.h
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
20 #ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
21 #define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
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"
34 class ArithVarNodeMap
{
37 * Bidirectional map between Nodes and ArithVars.
39 NodeToArithVarMap d_nodeToArithVarMap
;
40 ArithVarToNodeMap d_arithVarToNodeMap
;
44 typedef ArithVarToNodeMap::const_iterator var_iterator
;
48 inline bool hasArithVar(TNode x
) const {
49 return d_nodeToArithVarMap
.find(x
) != d_nodeToArithVarMap
.end();
52 inline bool hasNode(ArithVar a
) const {
53 return d_arithVarToNodeMap
.isKey(a
);
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
;
62 inline Node
asNode(ArithVar a
) const{
64 return d_arithVarToNodeMap
[a
];
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
;
74 inline void remove(ArithVar x
){
76 Node node
= asNode(x
);
78 d_nodeToArithVarMap
.erase(d_nodeToArithVarMap
.find(node
));
79 d_arithVarToNodeMap
.remove(x
);
82 var_iterator
var_begin() const {
83 return d_arithVarToNodeMap
.begin();
85 var_iterator
var_end() const {
86 return d_arithVarToNodeMap
.end();
89 };/* class ArithVarNodeMap */
91 }/* CVC4::theory::arith namespace */
92 }/* CVC4::theory namespace */
95 #endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */