diff options
author | Tim King <taking@cs.nyu.edu> | 2012-10-19 19:26:31 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-10-19 19:26:31 +0000 |
commit | 15dd90e7101ae199f15d4ed9976428c93e98cee0 (patch) | |
tree | 89623cf093e5ec013a17d0737b0f6be048ee63b0 /src/theory/theory.h | |
parent | 5796f9398adfab80860f17f4c99f143801689d56 (diff) |
Fix for model building with shared terms for arithmetic.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index a57f7646d..e51b8594e 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -38,6 +38,7 @@ #include <iostream> #include <strings.h> +#include <ext/hash_set> namespace CVC4 { @@ -785,6 +786,12 @@ public: return d_sharedTerms.end(); } + + /** + * This is a utility function for constructing a copy of the currently shared terms + * in a queriable form. As this is + */ + std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const; };/* class Theory */ std::ostream& operator<<(std::ostream& os, Theory::Effort level); @@ -804,6 +811,8 @@ public: protected: /** reference to the instantiation engine */ QuantifiersEngine* d_quantEngine; + + public: InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){} virtual ~InstStrategy(){} |