From 2a4827990b1e083a0351f4f86de6889d0bb21719 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 15 Aug 2018 12:16:20 -0700 Subject: [PATCH] Remove unused tuple classes (#2313) Since we are using C++11, we can replace the triple and quad classes with std::tuple. --- src/smt/smt_engine.cpp | 22 ++++--- src/theory/arrays/array_info.h | 10 ++- src/theory/arrays/theory_arrays.cpp | 30 ++++----- src/theory/arrays/theory_arrays.h | 3 +- src/util/Makefile.am | 1 - src/util/ntuple.h | 98 ----------------------------- 6 files changed, 33 insertions(+), 131 deletions(-) delete mode 100644 src/util/ntuple.h 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 #include #include +#include #include #include #include @@ -2775,18 +2776,21 @@ void SmtEnginePrivate::finishInit() Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) { - stack< triple > worklist; + stack> worklist; stack 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 #include +#include #include #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 CTNodeList; -typedef quad RowLemmaType; +using RowLemmaType = std::tuple; 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 ("<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 ("<getLevel()) <<"Arrays::checkRowForIndex ("<getLevel()) <<"Arrays::checkRowForIndex ("<getLevel()) <<"Arrays::checkRowLemmas ("<getLevel()) <<"Arrays::checkRowLemmas ("< RowLemmaType; + using RowLemmaType = std::tuple; context::CDQueue d_RowQueue; context::CDHashSet 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 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 -inline triple -make_triple(const T1& t1, const T2& t2, const T3& t3) { - return triple(t1, t2, t3); -}/* make_triple() */ - -template -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 -bool operator==(const quad& x, - const quad& y) { - return (x.first==y.first && x.second==y.second && - x.third == y.third && x.fourth==y.fourth); -} - -template -bool operator<(const quad& x, - const quad& 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 -inline quad -make_quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) { - return quad(t1, t2, t3, t4); -}/* make_quad() */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__NTUPLE_H */ -- 2.30.2