diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 4e3bba501..30c4dabdf 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -29,6 +29,8 @@ #include <ext/hash_set> #include <iostream> #include <map> +#include "context/cdchunk_list.h" +#include "context/cdhashset.h" namespace CVC4 { @@ -113,8 +115,11 @@ class QuantifiersEngine { friend class quantifiers::RewriteEngine; friend class quantifiers::QuantConflictFind; friend class inst::InstMatch; -private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; + typedef context::CDChunkList<Node> NodeList; + typedef context::CDChunkList<bool> BoolList; + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; +private: /** reference to theory engine object */ TheoryEngine* d_te; /** vector of modules for quantifiers */ @@ -197,9 +202,10 @@ private: /** has presolve been called */ context::CDO< bool > d_presolve; /** presolve cache */ - std::vector< Node > d_presolve_cache; - std::vector< bool > d_presolve_cache_wq; - std::vector< bool > d_presolve_cache_wic; + NodeSet d_presolve_in; + NodeList d_presolve_cache; + BoolList d_presolve_cache_wq; + BoolList d_presolve_cache_wic; private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: |