parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

1 files changed, 8 insertions, 0 deletions

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 7e382697c..02418d3df 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__CONTEXT__CDLIST_H
 #define __CVC4__CONTEXT__CDLIST_H
 
+#include <iterator>
+
 #include "context/context.h"
 #include "util/Assert.h"
 
@@ -224,6 +226,12 @@ public:
 
   public:
 
+    typedef std::input_iterator_tag iterator_category;
+    typedef T value_type;
+    typedef ptrdiff_t difference_type;
+    typedef const T* pointer;
+    typedef const T& reference;
+
     const_iterator() : d_it(NULL) {}
 
     inline bool operator==(const const_iterator& i) const {