From ef7b7bba7bc9b207d5a2198518f21b13490caa32 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 28 Sep 2015 16:18:32 +0200
Subject: Improve quantifiers engine wrt incremental presolve. Add regressions.

---
 src/theory/quantifiers_engine.h | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'src/theory/quantifiers_engine.h')

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:
-- 
cgit v1.2.3