fix deprecation of std::iterator (#7332)

When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;

difference_type	        Iter::difference_type
value_type	        Iter::value_type
pointer	                Iter::pointer
reference	        Iter::reference
iterator_category	Iter::iterator_category

```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.

This pull request performs the fix, and the program is semantically equivalent before and after the fix.

References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 73b3d1ee9866c48853e5e60e0ea3b24dc8955c94..3db581db64aafa93b0b7781b33027272c2904b05 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1167,11 +1167,30 @@ class CVC5_EXPORT Term
    *       for example, the term f(x, y) will have Kind APPLY_UF and three
    *       children: f, x, and y
    */
-  class const_iterator : public std::iterator<std::input_iterator_tag, Term>
+  class const_iterator
   {
     friend class Term;
 
    public:
+    /* The following types are required by trait std::iterator_traits */
+
+    /** Iterator tag */
+    using iterator_category = std::forward_iterator_tag;
+
+    /** The type of the item */
+    using value_type = Term;
+
+    /** The pointer type of the item */
+    using pointer = const Term*;
+
+    /** The reference type of the item */
+    using reference = const Term&;
+
+    /** The type returned when two iterators are subtracted */
+    using difference_type = std::ptrdiff_t;
+
+    /* End of std::iterator_traits required types */
+
     /**
      * Null Constructor.
      */
@@ -1951,11 +1970,29 @@ class CVC5_EXPORT DatatypeConstructor
    * Iterator for the selectors of a datatype constructor.
    */
   class const_iterator
-      : public std::iterator<std::input_iterator_tag, DatatypeConstructor>
   {
     friend class DatatypeConstructor;  // to access constructor
 
    public:
+    /* The following types are required by trait std::iterator_traits */
+
+    /** Iterator tag */
+    using iterator_category = std::forward_iterator_tag;
+
+    /** The type of the item */
+    using value_type = DatatypeConstructor;
+
+    /** The pointer type of the item */
+    using pointer = const DatatypeConstructor*;
+
+    /** The reference type of the item */
+    using reference = const DatatypeConstructor&;
+
+    /** The type returned when two iterators are subtracted */
+    using difference_type = std::ptrdiff_t;
+
+    /* End of std::iterator_traits required types */
+
     /** Nullary constructor (required for Cython). */
     const_iterator();
 
@@ -2184,11 +2221,30 @@ class CVC5_EXPORT Datatype
   /**
    * Iterator for the constructors of a datatype.
    */
-  class const_iterator : public std::iterator<std::input_iterator_tag, Datatype>
+  class const_iterator
   {
     friend class Datatype;  // to access constructor
 
    public:
+    /* The following types are required by trait std::iterator_traits */
+
+    /** Iterator tag */
+    using iterator_category = std::forward_iterator_tag;
+
+    /** The type of the item */
+    using value_type = Datatype;
+
+    /** The pointer type of the item */
+    using pointer = const Datatype*;
+
+    /** The reference type of the item */
+    using reference = const Datatype&;
+
+    /** The type returned when two iterators are subtracted */
+    using difference_type = std::ptrdiff_t;
+
+    /* End of std::iterator_traits required types */
+
     /** Nullary constructor (required for Cython). */
     const_iterator();
 

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 16c3a09e306c0a76946f488daf711e1cb0e30db7..d765905d6632db0ec83c3b42ee994826b53863d0 100644 (file)
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -421,7 +421,7 @@ class CDHashMap : public ContextObj
     const Element* d_it;
 
    public:
-    using iterator_category = std::input_iterator_tag;
+    using iterator_category = std::forward_iterator_tag;
     using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
     using difference_type = ptrdiff_t;
     using pointer = typename CDOhash_map<Key, Data, HashFcn>::value_type*;

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 007acc64d14e0c4ce34dc7311b370fe5c95bfb43..997dbc924222b612abf474cc4edf76c20642516a 100644 (file)
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -384,7 +384,7 @@ protected:
 
     // FIXME we support operator--, but do we satisfy all the
     // requirements of a bidirectional iterator ?
-    typedef std::input_iterator_tag iterator_category;
+    typedef std::bidirectional_iterator_tag iterator_category;
     typedef T value_type;
     typedef std::ptrdiff_t difference_type;
     typedef const T* pointer;

diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index de6082ead82dd27b812422f46f08929bee9cc28b..945038fbfe76389f1a866674427dbc6a9b1056d4 100644 (file)
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -26,11 +26,30 @@
 namespace cvc5 {
 namespace expr {
 
-class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> {
+class NodeSelfIterator {
   Node d_node;
   Node::const_iterator d_child;
 
 public:
+  /* The following types are required by trait std::iterator_traits */
+
+  /** Iterator tag */
+  using iterator_category = std::forward_iterator_tag;
+
+  /** The type of the item */
+  using value_type = Node;
+
+  /** The pointer type of the item */
+  using pointer = Node*;
+
+  /** The reference type of the item */
+  using reference = Node&;
+
+  /** The type returned when two iterators are subtracted */
+  using difference_type = std::ptrdiff_t;
+
+  /* End of std::iterator_traits required types */
+
   static NodeSelfIterator self(TNode n);
   static NodeSelfIterator selfEnd(TNode n);
 

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 76a94f4c509aa72722b247f45046870464ea8537..4084ed11c5d3f097d97169e3f450a6755433ed79 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -473,11 +473,30 @@ private:
 
 public:
 
-  class iterator : public std::iterator<std::input_iterator_tag, Variable> {
+  class iterator {
   private:
     internal_iterator d_iter;
 
   public:
+    /* The following types are required by trait std::iterator_traits */
+
+    /** Iterator tag */
+    using iterator_category = std::forward_iterator_tag;
+
+    /** The type of the item */
+    using value_type = Variable;
+
+    /** The pointer type of the item */
+    using pointer = Variable*;
+
+    /** The reference type of the item */
+    using reference = Variable&;
+
+    /** The type returned when two iterators are subtracted */
+    using difference_type = std::ptrdiff_t;
+
+    /* End of std::iterator_traits required types */
+
     explicit iterator(internal_iterator i) : d_iter(i) {}
 
     inline Variable operator*() {
@@ -800,11 +819,30 @@ private:
 public:
   static bool isMember(TNode n);
 
-  class iterator : public std::iterator<std::input_iterator_tag, Monomial> {
+  class iterator {
   private:
     internal_iterator d_iter;
 
   public:
+    /* The following types are required by trait std::iterator_traits */
+
+    /** Iterator tag */
+    using iterator_category = std::forward_iterator_tag;
+
+    /** The type of the item */
+    using value_type = Monomial;
+
+    /** The pointer type of the item */
+    using pointer = Monomial*;
+
+    /** The reference type of the item */
+    using reference = Monomial&;
+
+    /** The type returned when two iterators are subtracted */
+    using difference_type = std::ptrdiff_t;
+
+    /* End of std::iterator_traits required types */
+
     explicit iterator(internal_iterator i) : d_iter(i) {}
 
     inline Monomial operator*() {

diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index 8dffaa533e0fe338d8af9b6519093e57f74ce63d..44b290a16bbd46cd02476b1cdf5b9756061e0346 100644 (file)
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -95,7 +95,27 @@ public:
 
   }; /* BinaryHeap<>::handle */
 
-  class const_iterator : public std::iterator<std::input_iterator_tag, Elem> {
+  class const_iterator {
+  public:
+    /* The following types are required by trait std::iterator_traits */
+
+    /** Iterator tag */
+    using iterator_category = std::forward_iterator_tag;
+
+    /** The type of the item */
+    using value_type = Elem;
+
+    /** The pointer type of the item */
+    using pointer = const Elem*;
+
+    /** The reference type of the item */
+    using reference = const Elem&;
+
+    /** The type returned when two iterators are subtracted */
+    using difference_type = std::ptrdiff_t;
+
+    /* End of std::iterator_traits required types */
+
   private:
     typename ElementVector::const_iterator d_iter;
     friend class BinaryHeap;