summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r--src/theory/arrays/theory_arrays.h3
1 files changed, 2 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback