diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/array_info.h | 10 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 30 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 3 |
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; |