#include <sstream>
#include <stack>
#include <string>
+#include <tuple>
#include <unordered_map>
#include <unordered_set>
#include <utility>
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
// 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 {
#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 {
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);
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);
}
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);
}
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);
}
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);
}
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);
}
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);
}
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) ||
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) ||
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();
#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#include <tuple>
#include <unordered_map>
#include "context/cdhashmap.h"
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;
index.cpp \
index.h \
maybe.h \
- ntuple.h \
ostream_util.cpp \
ostream_util.h \
proof.h \
+++ /dev/null
-/********************* */
-/*! \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 */
projects / cvc5.git / commitdiff