diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /src/theory/substitutions.h | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
Diffstat (limited to 'src/theory/substitutions.h')
-rw-r--r-- | src/theory/substitutions.h | 49 |
1 files changed, 25 insertions, 24 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 849c8f166..253507645 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -24,7 +24,11 @@ #include <utility> #include <vector> #include <algorithm> + #include "expr/node.h" +#include "context/context.h" +#include "context/cdo.h" +#include "context/cdmap.h" namespace CVC4 { namespace theory { @@ -32,17 +36,22 @@ namespace theory { /** * The type for the Substitutions mapping output by * Theory::simplify(), TheoryEngine::simplify(), and - * Valuation::simplify(). This is in its own header to avoid circular - * dependences between those three. + * Valuation::simplify(). This is in its own header to + * avoid circular dependences between those three. + * + * This map is context-dependent. */ class SubstitutionMap { public: - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap; private: + /** The context within which this SubstitutionMap was constructed. */ + context::Context* d_context; + /** The variables, in order of addition */ NodeMap d_substitutions; @@ -50,14 +59,19 @@ private: NodeMap d_substitutionCache; /** Has the cache been invalidated */ - bool d_cacheInvalidated; + context::CDO<bool> d_cacheInvalidated; - /** Internaal method that performs substitution */ + /** Internal method that performs substitution */ Node internalSubstitute(TNode t, NodeMap& substitutionCache); public: - SubstitutionMap(): d_cacheInvalidated(true) {} + SubstitutionMap(context::Context* context) : + d_context(context), + d_substitutions(context), + d_substitutionCache(context), + d_cacheInvalidated(context) { + } /** * Adds a substitution from x to t @@ -77,24 +91,11 @@ public: return const_cast<SubstitutionMap*>(this)->apply(t); } - /** - * Clear out the accumulated substitutions, resetting this - * SubstitutionMap to the way it was when first constructed. - */ - void clear() { - d_substitutions.clear(); - d_substitutionCache.clear(); - d_cacheInvalidated = true; - } - - /** - * Swap the contents of this SubstitutionMap with those of another. - */ - void swap(SubstitutionMap& map) { - d_substitutions.swap(map.d_substitutions); - d_substitutionCache.swap(map.d_substitutionCache); - std::swap(d_cacheInvalidated, map.d_cacheInvalidated); - } + // NOTE [MGD]: removed clear() and swap() from the interface + // when this data structure became context-dependent + // because they weren't used---and it's not clear how they + // should // best interact with cache invalidation on context + // pops. /** * Print to the output stream |