Remove unused tuple classes (#2313)

Since we are using C++11, we can replace the triple and quad classes
with std::tuple.

6 files changed, 33 insertions, 131 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cc6f09801..db4efe89f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -23,6 +23,7 @@
 #include <sstream>
 #include <stack>
 #include <string>
+#include <tuple>
 #include <unordered_map>
 #include <unordered_set>
 #include <utility>
@@ -2775,18 +2776,21 @@ void SmtEnginePrivate::finishInit()
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
 {
-  stack< triple<Node, Node, bool> > worklist;
+  stack<std::tuple<Node, Node, bool>> worklist;
   stack<Node> result;
-  worklist.push(make_triple(Node(n), Node(n), false));
+  worklist.push(std::make_tuple(Node(n), Node(n), false));
   // The worklist is made of triples, each is input / original node then the output / rewritten node
   // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
   // or upward pass).
 
   do {
     spendResource(options::preprocessStep());
-    n = worklist.top().first;                      // n is the input / original
-    Node node = worklist.top().second;             // node is the output / result
-    bool childrenPushed = worklist.top().third;
+
+    // n is the input / original
+    // node is the output / result
+    Node node;
+    bool childrenPushed;
+    std::tie(n, node, childrenPushed) = worklist.top();
     worklist.pop();
 
     // Working downwards
@@ -2910,10 +2914,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
 
       // the partial functions can fall through, in which case we still
       // consider their children
-      worklist.push(make_triple(Node(n), node, true));            // Original and rewritten result
+      worklist.push(std::make_tuple(
+          Node(n), node, true));  // Original and rewritten result
 
       for(size_t i = 0; i < node.getNumChildren(); ++i) {
-        worklist.push(make_triple(node[i], node[i], false));      // Rewrite the children of the result only
+        worklist.push(
+            std::make_tuple(node[i],
+                            node[i],
+                            false));  // Rewrite the children of the result only
       }
 
     } else {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index ec0e1765a..ed8594ca7 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -20,13 +20,13 @@
 
 #include <iostream>
 #include <map>
+#include <tuple>
 #include <unordered_map>
 
 #include "context/backtrackable.h"
 #include "context/cdlist.h"
 #include "context/cdhashmap.h"
 #include "expr/node.h"
-#include "util/ntuple.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -34,14 +34,12 @@ namespace theory {
 namespace arrays {
 
 typedef context::CDList<TNode> CTNodeList;
-typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
+using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
 
 struct RowLemmaTypeHashFunction {
   size_t operator()(const RowLemmaType& q) const {
-    TNode n1 = q.first;
-    TNode n2 = q.second;
-    TNode n3 = q.third;
-    TNode n4 = q.fourth;
+    TNode n1, n2, n3, n4;
+    std::tie(n1, n2, n3, n4) = q;
     return (size_t) (n1.getId()*0x9e3779b9 + n2.getId()*0x30000059 +
         n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c98c36f13..9af564a05 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1609,7 +1609,7 @@ void TheoryArrays::setNonLinear(TNode a)
       Assert(store.getKind() == kind::STORE);
       TNode j = store[1];
       TNode c = store[0];
-      lem = make_quad(store, c, j, i);
+      lem = std::make_tuple(store, c, j, i);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(lem);
     }
@@ -1836,7 +1836,7 @@ void TheoryArrays::checkStore(TNode a) {
     for(; it < js->size(); ++it) {
       TNode j = (*js)[it];
       if (i == j) continue;
-      lem = make_quad(a,b,i,j);
+      lem = std::make_tuple(a, b, i, j);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
       queueRowLemma(lem);
     }
@@ -1877,7 +1877,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     Assert(store.getKind()==kind::STORE);
     TNode j = store[1];
     if (i == j) continue;
-    lem = make_quad(store, store[0], j, i);
+    lem = std::make_tuple(store, store[0], j, i);
     Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
     queueRowLemma(lem);
   }
@@ -1889,7 +1889,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
       Assert(instore.getKind()==kind::STORE);
       TNode j = instore[1];
       if (i == j) continue;
-      lem = make_quad(instore, instore[0], j, i);
+      lem = std::make_tuple(instore, instore[0], j, i);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(lem);
     }
@@ -1936,7 +1936,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
       Assert(store.getKind() == kind::STORE);
       TNode j = store[1];
       TNode c = store[0];
-      lem = make_quad(store, c, j, i);
+      lem = std::make_tuple(store, c, j, i);
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(lem);
     }
@@ -1951,7 +1951,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
         Assert(store.getKind() == kind::STORE);
         TNode j = store[1];
         TNode c = store[0];
-        lem = make_quad(store, c, j, i);
+        lem = std::make_tuple(store, c, j, i);
         Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
         queueRowLemma(lem);
       }
@@ -1965,10 +1965,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
   Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
                      << options::arraysPropagate() << std::endl;
 
-  TNode a = lem.first;
-  TNode b = lem.second;
-  TNode i = lem.third;
-  TNode j = lem.fourth;
+  TNode a, b, i, j;
+  std::tie(a, b, i, j) = lem;
 
   Assert(a.getType().isArray() && b.getType().isArray());
   if (d_equalityEngine.areEqual(a,b) ||
@@ -2024,10 +2022,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
     return;
   }
-  TNode a = lem.first;
-  TNode b = lem.second;
-  TNode i = lem.third;
-  TNode j = lem.fourth;
+  TNode a, b, i, j;
+  std::tie(a, b, i, j) = lem;
 
   Assert(a.getType().isArray() && b.getType().isArray());
   if (d_equalityEngine.areEqual(a,b) ||
@@ -2156,10 +2152,8 @@ bool TheoryArrays::dischargeLemmas()
       continue;
     }
 
-    TNode a = l.first;
-    TNode b = l.second;
-    TNode i = l.third;
-    TNode j = l.fourth;
+    TNode a, b, i, j;
+    std::tie(a, b, i, j) = l;
     Assert(a.getType().isArray() && b.getType().isArray());
 
     NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index aca4cbcb9..363ad16ff 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
+#include <tuple>
 #include <unordered_map>
 
 #include "context/cdhashmap.h"
@@ -369,7 +370,7 @@ class TheoryArrays : public Theory {
 
   bool d_mergeInProgress;
 
-  typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
+  using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
 
   context::CDQueue<RowLemmaType> d_RowQueue;
   context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 04d0a5b02..baa3286ab 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -35,7 +35,6 @@ libutil_la_SOURCES = \
 	index.cpp \
 	index.h \
 	maybe.h \
-	ntuple.h \
 	ostream_util.cpp \
 	ostream_util.h \
 	proof.h \
diff --git a/src/util/ntuple.h b/src/util/ntuple.h
deleted file mode 100644
index 1df8c8e76..000000000
--- a/src/util/ntuple.h
+++ /dev/null
@@ -1,98 +0,0 @@
-/*********************                                                        */
-/*! \file ntuple.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Similar to std::pair<>, for triples and quadruples
- **
- ** Similar to std::pair<>, for triples and quadruples.  Once we move to c++0x, this
- ** can be removed in favor of (standard-provided) N-ary tuples.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__NTUPLE_H
-#define __CVC4__NTUPLE_H
-
-namespace CVC4 {
-
-template <class T1, class T2, class T3>
-class triple {
-public:
-  T1 first;
-  T2 second;
-  T3 third;
-  triple() {}
-  triple(const T1& t1, const T2& t2, const T3& t3) :
-    first(t1),
-    second(t2),
-    third(t3) {
-  }
-};/* class triple<> */
-
-template <class T1, class T2, class T3>
-inline triple<T1, T2, T3>
-make_triple(const T1& t1, const T2& t2, const T3& t3) {
-  return triple<T1, T2, T3>(t1, t2, t3);
-}/* make_triple() */
-
-template <class T1, class T2, class T3, class T4>
-class quad {
-public:
-  T1 first;
-  T2 second;
-  T3 third;
-  T4 fourth;
-  quad() {}
-  quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) :
-    first(t1),
-    second(t2),
-    third(t3),
-    fourth(t4) {
-  }
-};/* class quad<> */
-
-template <class T1, class T2, class T3, class T4>
-bool operator==(const quad<T1,T2,T3,T4>& x,
-                const quad<T1,T2,T3,T4>& y) {
-  return (x.first==y.first   && x.second==y.second &&
-          x.third == y.third && x.fourth==y.fourth);
-}
-
-template <class T1, class T2, class T3, class T4>
-bool operator<(const quad<T1,T2,T3,T4>& x,
-                const quad<T1,T2,T3,T4>& y) {
-  if(x.first< y.first) {
-    return true;
-  }
-  else if (x.first == y.first) {
-    if(x.second < y.second) {
-      return true;
-    }
-    else if(y.second == y.second) {
-      if(x.third < y.third) {
-        return true;
-      }
-      else if (x.fourth < y.fourth) {
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-template <class T1, class T2, class T3, class T4>
-inline quad<T1, T2, T3, T4>
-make_quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) {
-  return quad<T1, T2, T3, T4>(t1, t2, t3, t4);
-}/* make_quad() */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__NTUPLE_H */