diff options
author | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
commit | abe849b486ea3707fd51a612c7982554f3d6581f (patch) | |
tree | 8f3967f644f9098079c778dd60cf9feb36e1ab2b /src/theory/arith/arithvar_node_map.h | |
parent | b90081962840584bb9eeda368ea232a7d42a292b (diff) |
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
Diffstat (limited to 'src/theory/arith/arithvar_node_map.h')
-rw-r--r-- | src/theory/arith/arithvar_node_map.h | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h new file mode 100644 index 000000000..aca61878d --- /dev/null +++ b/src/theory/arith/arithvar_node_map.h @@ -0,0 +1,59 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H +#define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H + + +#include "theory/arith/arith_utilities.h" +#include "context/context.h" +#include "context/cdlist.h" +#include "context/cdmap.h" +#include "context/cdo.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithVarNodeMap { +private: + /** + * Bidirectional map between Nodes and ArithVars. + */ + NodeToArithVarMap d_nodeToArithVarMap; + ArithVarToNodeMap d_arithVarToNodeMap; + +public: + ArithVarNodeMap() {} + + inline bool hasArithVar(TNode x) const { + return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); + } + + 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; + } + + inline void setArithVar(TNode x, ArithVar a){ + Assert(!hasArithVar(x)); + Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); + d_arithVarToNodeMap[a] = x; + d_nodeToArithVarMap[x] = a; + } + + const ArithVarToNodeMap& getArithVarToNodeMap() const { + return d_arithVarToNodeMap; + } + +};/* class ArithVarNodeMap */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */ |