Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 22 insertions, 0 deletions

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index c03baa1ac..1ade4815d 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -48,6 +48,9 @@ public:
 
   typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
 
+  typedef NodeMap::iterator iterator;
+  typedef NodeMap::const_iterator const_iterator;
+
 private:
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
@@ -115,6 +118,22 @@ public:
     return const_cast<SubstitutionMap*>(this)->apply(t);
   }
 
+  iterator begin() {
+    return d_substitutions.begin();
+  }
+
+  iterator end() {
+    return d_substitutions.end();
+  }
+
+  const_iterator begin() const {
+    return d_substitutions.begin();
+  }
+
+  const_iterator end() const {
+    return d_substitutions.end();
+  }
+
   // 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
@@ -134,6 +153,9 @@ inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subs
 }
 
 }/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__SUBSTITUTIONS_H */