Remove unused tuple classes (#2313)

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

3 files changed, 18 insertions, 25 deletions

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;