1 files changed, 37 insertions, 19 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index f501dba21..0f4b55d4a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -28,6 +28,8 @@
 #include <string>
 #include <iostream>
 #include <utility>
+#include <algorithm>
+#include <functional>
 #include <stdint.h>
 
 #include "expr/type.h"
@@ -832,16 +834,23 @@ public:
    */
   inline bool hasSubterm(NodeTemplate<false> t, bool strict = false) const;
 
-  NodeTemplate<true> eqNode(const NodeTemplate& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
 
   NodeTemplate<true> notNode() const;
-  NodeTemplate<true> andNode(const NodeTemplate& right) const;
-  NodeTemplate<true> orNode(const NodeTemplate& right) const;
-  NodeTemplate<true> iteNode(const NodeTemplate& thenpart,
-                             const NodeTemplate& elsepart) const;
-  NodeTemplate<true> iffNode(const NodeTemplate& right) const;
-  NodeTemplate<true> impNode(const NodeTemplate& right) const;
-  NodeTemplate<true> xorNode(const NodeTemplate& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2, bool ref_count3>
+  NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
+                             const NodeTemplate<ref_count3>& elsepart) const;
+  template <bool ref_count2>
+  NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
+  template <bool ref_count2>
+  NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
 
 };/* class NodeTemplate<ref_count> */
 
@@ -1085,8 +1094,9 @@ operator=(const NodeTemplate<!ref_count>& e) {
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
 }
@@ -1098,44 +1108,50 @@ NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2, bool ref_count3>
 NodeTemplate<true>
-NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count>& thenpart,
-                                 const NodeTemplate<ref_count>& elsepart) const {
+NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
+                                 const NodeTemplate<ref_count3>& elsepart) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
 }
 
 template <bool ref_count>
+template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const {
+NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
 }
@@ -1273,11 +1289,13 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
   }
 
   // otherwise compute
-  Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin,
+  Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd),
           "Substitution iterator ranges must be equal size" );
-  Iterator1 j = find(nodesBegin, nodesEnd, *this);
+  Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this));
   if(j != nodesEnd) {
-    Node n = *(replacementsBegin + (j - nodesBegin));
+    Iterator2 b = replacementsBegin;
+    std::advance(b, std::distance(nodesBegin, j));
+    Node n = *b;
     cache[*this] = n;
     return n;
   } else if(getNumChildren() == 0) {