diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-28 16:18:32 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-28 16:18:32 +0200 |
| commit | ef7b7bba7bc9b207d5a2198518f21b13490caa32 (patch) | |
| tree | 43867e7dcab54bd77bc07167e096cc518b0be035 /src/theory/quantifiers_engine.h | |
| parent | 187e5d57adeda59c8899321c882db1d5b9a6f2ba (diff) | |
Improve quantifiers engine wrt incremental presolve. Add regressions.
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: |