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 

6 files changed, 142 insertions, 9 deletions

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 73b3d1ee9..3db581db6 100644
--- 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 16c3a09e3..d765905d6 100644
--- 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 007acc64d..997dbc924 100644
--- 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 de6082ead..945038fbf 100644
--- 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 76a94f4c5..4084ed11c 100644
--- 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 8dffaa533..44b290a16 100644
--- 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;