diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 22 |
1 files changed, 15 insertions, 7 deletions
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 <sstream> #include <stack> #include <string> +#include <tuple> #include <unordered_map> #include <unordered_set> #include <utility> @@ -2775,18 +2776,21 @@ void SmtEnginePrivate::finishInit() 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 @@ -2910,10 +2914,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node // 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 { |