diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
commit | bd0a6c39c56c6ad2bf12e7b9fd41db1772fed9cd (patch) | |
tree | 51f4bc5994a0716e6f4cfeed136360954ce505ac /src/theory/arith/arithvar_node_map.h | |
parent | 356a8b6e5ea2622d0fef5cf209159caf08ba5297 (diff) |
Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.
Diffstat (limited to 'src/theory/arith/arithvar_node_map.h')
-rw-r--r-- | src/theory/arith/arithvar_node_map.h | 31 |
1 files changed, 25 insertions, 6 deletions
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index 3a2cff236..e0e589e57 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -40,31 +40,50 @@ private: ArithVarToNodeMap d_arithVarToNodeMap; public: + + typedef ArithVarToNodeMap::const_iterator var_iterator; + ArithVarNodeMap() {} inline bool hasArithVar(TNode x) const { return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); } + inline bool hasNode(ArithVar a) const { + return d_arithVarToNodeMap.isKey(a); + } + inline ArithVar asArithVar(TNode x) const{ Assert(hasArithVar(x)); Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); return (d_nodeToArithVarMap.find(x))->second; } + inline Node asNode(ArithVar a) const{ - Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end()); - return (d_arithVarToNodeMap.find(a))->second; + Assert(hasNode(a)); + return d_arithVarToNodeMap[a]; } inline void setArithVar(TNode x, ArithVar a){ Assert(!hasArithVar(x)); - Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); - d_arithVarToNodeMap[a] = x; + Assert(!d_arithVarToNodeMap.isKey(a)); + d_arithVarToNodeMap.set(a, x); d_nodeToArithVarMap[x] = a; } - const ArithVarToNodeMap& getArithVarToNodeMap() const { - return d_arithVarToNodeMap; + inline void remove(ArithVar x){ + Assert(hasNode(x)); + Node node = asNode(x); + + d_nodeToArithVarMap.erase(d_nodeToArithVarMap.find(node)); + d_arithVarToNodeMap.remove(x); + } + + var_iterator var_begin() const { + return d_arithVarToNodeMap.begin(); + } + var_iterator var_end() const { + return d_arithVarToNodeMap.end(); } };/* class ArithVarNodeMap */ |