From 81faaf4023cd29af4fca72607dd59d1ab49821a0 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 31 Aug 2016 15:58:21 -0700 Subject: [PATCH] Removing the usage of typeof from theory_sets_private. --- src/theory/sets/theory_sets_private.cpp | 236 +++++++++++++----------- src/theory/sets/theory_sets_private.h | 5 +- 2 files changed, 135 insertions(+), 106 deletions(-) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index a16e857dd..5f6a38032 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -217,7 +217,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt) if(x.getType().isSet()) { if(polarity) { const CDTNodeList* l = d_termInfoManager->getNonMembers(S); - for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + for(CDTNodeList::iterator it = l->begin(); it != l->end(); ++it) { TNode n = *it; learnLiteral( /* atom = */ EQUAL(x, n), /* polarity = */ false, @@ -225,7 +225,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt) } } else { const CDTNodeList* l = d_termInfoManager->getMembers(S); - for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + for(CDTNodeList::iterator it = l->begin(); it != l->end(); ++it) { TNode n = *it; learnLiteral( /* atom = */ EQUAL(x, n), /* polarity = */ false, @@ -254,7 +254,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt) Debug("sets-prop") << "[sets-prop] Propagating 'up' for " << x << element_of_str << S << std::endl; const CDTNodeList* parentList = d_termInfoManager->getParents(S); - for(typeof(parentList->begin()) k = parentList->begin(); + for(CDTNodeList::const_iterator k = parentList->begin(); k != parentList->end(); ++k) { doSettermPropagation(x, *k); if(d_conflict) return; @@ -474,9 +474,15 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const context::CDList::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end(); - std::map > equalities; - std::set< pair > disequalities; - std::map, std::set > > members; + typedef std::set TNodeSet; + + typedef std::map EqualityMap; + EqualityMap equalities; + + typedef std::set< std::pair > TNodePairSet; + TNodePairSet disequalities; + typedef std::map > MemberMap; + MemberMap members; static std::map numbering; static int number = 0; @@ -503,10 +509,14 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const (polarity ? members[right].first : members[right].second).insert(left); } } -#define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it)) - FORIT(kt, equalities) { + //#define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it)) + //FORIT(kt, equalities) + for(EqualityMap::const_iterator kt =equalities.begin(); kt != equalities.end(); ++kt) { Trace(tag) << " Eq class of t" << numbering[(*kt).first] << ": " << std::endl; - FORIT(jt, (*kt).second) { + + //FORIT(jt, (*kt).second) + const TNodeSet& kt_second = (*kt).second; + for(TNodeSet::const_iterator jt=kt_second.begin(); jt != kt_second.end(); ++jt) { TNode S = (*jt); if( S.getKind() != kind::UNION && S.getKind() != kind::INTERSECTION && S.getKind() != kind::SETMINUS) { Trace(tag) << " " << *jt << ((*jt).getType().isSet() ? "\n": " "); @@ -528,11 +538,19 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const } Trace(tag) << std::endl; } - FORIT(kt, disequalities) Trace(tag) << "NOT(t"< 0) { - Trace(tag) << "IN t" << numbering[(*kt).first] << ": "; - FORIT(jt, (*kt).second.first) { + //FORIT(kt, disequalities) + for(TNodePairSet::const_iterator kt=disequalities.begin(); kt != disequalities.end(); ++kt){ + Trace(tag) << "NOT(t"< 0) { + Trace(tag) << "IN t" << numbering[kt_key] << ": "; + //FORIT(jt, (*kt).second.first) + for(TNodeSet::const_iterator jt=kt_in_set.begin(); jt != kt_in_set.end(); ++jt) { TNode x = (*jt); if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) { Trace(tag) << x << ", "; @@ -542,9 +560,10 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const } Trace(tag) << std::endl; } - if( (*kt).second.second.size() > 0) { - Trace(tag) << "NOT IN t" << numbering[(*kt).first] << ": "; - FORIT(jt, (*kt).second.second) { + if( kt_out_set.size() > 0) { + Trace(tag) << "NOT IN t" << numbering[kt_key] << ": "; + //FORIT(jt, (*kt).second.second) + for(TNodeSet::const_iterator jt=kt_out_set.begin(); jt != kt_out_set.end(); ++jt){ TNode x = (*jt); if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) { Trace(tag) << x << ", "; @@ -556,7 +575,7 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const } } Trace(tag) << std::endl; -#undef FORIT + //#undef FORIT } void TheorySetsPrivate::computeCareGraph() { @@ -796,14 +815,15 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con return cur; } } -Node TheorySetsPrivate::elementsToShape(set elements, TypeNode setType) const + +Node TheorySetsPrivate::elementsToShape(std::set elements, TypeNode setType) const { NodeManager* nm = NodeManager::currentNM(); if(elements.size() == 0) { return nm->mkConst(EmptySet(nm->toType(setType))); } else { - typeof(elements.begin()) it = elements.begin(); + std::set::const_iterator it = elements.begin(); Node cur = SINGLETON(*it); while( ++it != elements.end() ) { cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it)); @@ -817,13 +837,13 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) Trace("sets-model") << "[sets-model] collectModelInfo(..., fullModel=" << (fullModel ? "true)" : "false)") << std::endl; - set terms; + std::set terms; NodeManager* nm = NodeManager::currentNM(); // // this is for processCard -- commenting out for now // if(Debug.isOn("sets-card")) { - // for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin(); + // for(CDNodeSet::const_iterator it = d_cardTerms.begin(); // it != d_cardTerms.end(); ++it) { // Debug("sets-card") << "[sets-card] " << *it << " = " // << d_external.d_valuation.getModelValue(*it) @@ -840,7 +860,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) //processCard2 begin if(Debug.isOn("sets-card")) { - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) { + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { Node n = nm->mkNode(kind::CARD, *it); Debug("sets-card") << "[sets-card] " << n << " = "; // if(d_external.d_sharedTerms.find(n) == d_external.d_sharedTerms.end()) continue; @@ -930,7 +950,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) //processCard2 begin leaves.clear(); - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) if(d_E.find(*it) == d_E.end()) leaves.insert(*it); d_statistics.d_numLeaves.setData(leaves.size()); @@ -1334,7 +1354,7 @@ void TheorySetsPrivate::propagate(Theory::Effort effort) { } const CDNodeSet& terms = (d_termInfoManager->d_terms); - for(typeof(terms.key_begin()) it = terms.key_begin(); it != terms.key_end(); ++it) { + for(CDNodeSet::key_iterator it = terms.key_begin(); it != terms.key_end(); ++it) { Node node = (*it); Kind k = node.getKind(); if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) { @@ -1490,14 +1510,14 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) void TheorySetsPrivate::presolve() { - for(typeof(d_termInfoManager->d_terms.begin()) it = d_termInfoManager->d_terms.begin(); + for(CDNodeSet::const_iterator it = d_termInfoManager->d_terms.begin(); it != d_termInfoManager->d_terms.end(); ++it) { d_relTerms.insert(*it); } if(Trace.isOn("sets-relterms")) { Trace("sets-relterms") << "[sets-relterms] "; - for(typeof(d_relTerms.begin()) it = d_relTerms.begin(); + for(CDNodeSet::const_iterator it = d_relTerms.begin(); it != d_relTerms.end(); ++it ) { Trace("sets-relterms") << (*it) << ", "; } @@ -1592,18 +1612,18 @@ void TheorySetsPrivate::TermInfoManager::mergeLists } } -TheorySetsPrivate::TermInfoManager::TermInfoManager -(TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq): - d_theory(theory), - d_context(satContext), - d_eqEngine(eq), - d_terms(satContext), - d_info() -{ } +TheorySetsPrivate::TermInfoManager::TermInfoManager( + TheorySetsPrivate& theory, context::Context* satContext, + eq::EqualityEngine* eq) + : d_theory(theory), + d_context(satContext), + d_eqEngine(eq), + d_terms(satContext), + d_info() {} TheorySetsPrivate::TermInfoManager::~TermInfoManager() { - for( typeof(d_info.begin()) it = d_info.begin(); - it != d_info.end(); ++it) { + for (SetsTermInfoMap::iterator it = d_info.begin(); it != d_info.end(); + ++it) { delete (*it).second; } } @@ -1664,14 +1684,14 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) { d_theory.registerCard(CARD(n)); } - typeof(d_info.begin()) ita = d_info.find(d_eqEngine->getRepresentative(n[i])); + SetsTermInfoMap::iterator ita = d_info.find(d_eqEngine->getRepresentative(n[i])); Assert(ita != d_info.end()); CDTNodeList* l = (*ita).second->elementsNotInThisSet; - for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + for(CDTNodeList::const_iterator it = l->begin(); it != l->end(); ++it) { d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) ); } l = (*ita).second->elementsInThisSet; - for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + for(CDTNodeList::const_iterator it = l->begin(); it != l->end(); ++it) { d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) ); } } @@ -1702,7 +1722,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue // propagation : parents const CDTNodeList* parentList = getParents(S); - for(typeof(parentList->begin()) k = parentList->begin(); + for(CDTNodeList::const_iterator k = parentList->begin(); k != parentList->end(); ++k) { d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k)); }// propagation : parents @@ -1770,8 +1790,8 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { << ", b: " << d_eqEngine->getRepresentative(b) << std::endl; - typeof(d_info.begin()) ita = d_info.find(a); - typeof(d_info.begin()) itb = d_info.find(b); + SetsTermInfoMap::iterator ita = d_info.find(a); + SetsTermInfoMap::iterator itb = d_info.find(b); Assert(ita != d_info.end()); Assert(itb != d_info.end()); @@ -1799,29 +1819,33 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { d_theory.d_modelCache.clear(); } -Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) -{ - if(d_terms.find(n) == d_terms.end()) { +Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) { + if (d_terms.find(n) == d_terms.end()) { return Node(); } Assert(n.getType().isSet()); - set elements, elements_const; + std::set elements; + std::set elements_const; Node S = d_eqEngine->getRepresentative(n); - typeof(d_theory.d_modelCache.begin()) it = d_theory.d_modelCache.find(S); - if(it != d_theory.d_modelCache.end()) { + context::CDHashMap::const_iterator it = + d_theory.d_modelCache.find(S); + if (it != d_theory.d_modelCache.end()) { return (*it).second; } const CDTNodeList* l = getMembers(S); - for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + for (CDTNodeList::const_iterator it = l->begin(); it != l->end(); ++it) { TNode n = *it; elements.insert(d_eqEngine->getRepresentative(n)); } - BOOST_FOREACH(TNode e, elements) { - if(e.isConst()) { + for(std::set::iterator it = elements.begin(); it != elements.end(); it++) { + TNode e = *it; + if (e.isConst()) { elements_const.insert(e); } else { Node eModelValue = d_theory.d_external.d_valuation.getModelValue(e); - if( eModelValue.isNull() ) return eModelValue; + if (eModelValue.isNull()) { + return eModelValue; + } elements_const.insert(eModelValue); } } @@ -1830,9 +1854,6 @@ Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) return v; } - - - /********************** Cardinality ***************************/ /********************** Cardinality ***************************/ /********************** Cardinality ***************************/ @@ -1847,7 +1868,7 @@ void TheorySetsPrivate::enableCard() cardCreateEmptysetSkolem(t); } - for(typeof(d_termInfoManager->d_terms.begin()) it = d_termInfoManager->d_terms.begin(); + for(CDNodeSet::const_iterator it = d_termInfoManager->d_terms.begin(); it != d_termInfoManager->d_terms.end(); ++it) { Node n = (*it); if(n.getKind() == kind::SINGLETON) { @@ -1864,7 +1885,7 @@ void TheorySetsPrivate::registerCard(TNode node) { // introduce cardinality of any set-term containing this term NodeManager* nm = NodeManager::currentNM(); const CDTNodeList* parentList = d_termInfoManager->getParents(node[0]); - for(typeof(parentList->begin()) it = parentList->begin(); + for(CDTNodeList::const_iterator it = parentList->begin(); it != parentList->end(); ++it) { registerCard(nm->mkNode(kind::CARD, *it)); } @@ -1891,9 +1912,10 @@ void TheorySetsPrivate::buildGraph() { edgesFd.clear(); edgesBk.clear(); disjoint.clear(); - - for(typeof(d_processedCardPairs.begin()) it = d_processedCardPairs.begin(); - it != d_processedCardPairs.end(); ++it) { + + for (std::map, bool>::const_iterator it = + d_processedCardPairs.begin(); + it != d_processedCardPairs.end(); ++it) { Node s = (it->first).first; Assert(Rewriter::rewrite(s) == s); Node t = (it->first).second; @@ -1908,7 +1930,7 @@ void TheorySetsPrivate::buildGraph() { tMs = Rewriter::rewrite(tMs); edgesFd[s].insert(sNt); - edgesFd[s].insert(sMt); + edgesFd[s].insert(sMt); edgesBk[sNt].insert(s); edgesBk[sMt].insert(s); @@ -1920,7 +1942,7 @@ void TheorySetsPrivate::buildGraph() { if(hasUnion) { Node sUt = nm->mkNode(kind::UNION, s, t); sUt = Rewriter::rewrite(sUt); - + edgesFd[sUt].insert(sNt); edgesFd[sUt].insert(sMt); edgesFd[sUt].insert(tMs); @@ -1937,32 +1959,34 @@ void TheorySetsPrivate::buildGraph() { disjoint.insert(make_pair(sMt, tMs)); } - if(Debug.isOn("sets-card-graph")) { + if (Debug.isOn("sets-card-graph")) { Debug("sets-card-graph") << "[sets-card-graph] Fd:" << std::endl; - for(typeof(edgesFd.begin()) it = edgesFd.begin(); - it != edgesFd.end(); ++it) { - Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) << std::endl; - for(typeof( (it->second).begin()) jt = (it->second).begin(); - jt != (it->second).end(); ++jt) { - Debug("sets-card-graph") << "[sets-card-graph] " << (*jt) << std::endl; + for (std::map >::const_iterator it = edgesFd.begin(); + it != edgesFd.end(); ++it) { + Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) + << std::endl; + for (std::set::const_iterator jt = (it->second).begin(); + jt != (it->second).end(); ++jt) { + Debug("sets-card-graph") << "[sets-card-graph] " << (*jt) + << std::endl; } } Debug("sets-card-graph") << "[sets-card-graph] Bk:" << std::endl; - for(typeof(edgesBk.begin()) it = edgesBk.begin(); - it != edgesBk.end(); ++it) { - Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) << std::endl; - for(typeof( (it->second).begin()) jt = (it->second).begin(); - jt != (it->second).end(); ++jt) { - Debug("sets-card-graph") << "[sets-card-graph] " << (*jt) << std::endl; + for (std::map >::const_iterator it = edgesBk.begin(); + it != edgesBk.end(); ++it) { + Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) + << std::endl; + for (std::set::const_iterator jt = (it->second).begin(); + jt != (it->second).end(); ++jt) { + Debug("sets-card-graph") << "[sets-card-graph] " << (*jt) + << std::endl; } } } - - leaves.clear(); - - for(typeof(d_processedCardTerms.begin()) it = d_processedCardTerms.begin(); + + for(CDNodeSet::const_iterator it = d_processedCardTerms.begin(); it != d_processedCardTerms.end(); ++it) { Node n = (*it)[0]; if( edgesFd.find(n) == edgesFd.end() ) { @@ -2167,7 +2191,7 @@ std::set TheorySetsPrivate::get_leaves(Node vertex1, Node vertex2, Node v Node TheorySetsPrivate::eqemptySoFar() { std::vector V; - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) { + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { Node rep = d_equalityEngine.getRepresentative(*it); if(rep.getKind() == kind::EMPTYSET) { V.push_back(EQUAL(rep, (*it))); @@ -2315,7 +2339,7 @@ void TheorySetsPrivate::print_graph() { std::string tag = "sets-graph"; if(Trace.isOn("sets-graph")) { Trace(tag) << "[sets-graph] Graph : " << std::endl; - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) { + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { TNode v = *it; // BOOST_FOREACH(TNode v, d_V) { Trace(tag) << "[" << tag << "] " << v << " : "; @@ -2334,7 +2358,7 @@ void TheorySetsPrivate::print_graph() { if(Trace.isOn("sets-graph-dot")) { std::ostringstream oss; oss << "digraph G { "; - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) { + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { TNode v = *it; if(d_E.find(v) != d_E.end()) { BOOST_FOREACH(TNode w, d_E[v].get()) { @@ -2368,7 +2392,7 @@ void TheorySetsPrivate::guessLeavesEmptyLemmas() { // Guess leaf nodes being empty or non-empty NodeManager* nm = NodeManager::currentNM(); leaves.clear(); - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) { + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { TNode v = *it; if(d_E.find(v) == d_E.end()) { leaves.insert(v); @@ -2385,7 +2409,7 @@ void TheorySetsPrivate::guessLeavesEmptyLemmas() { numLeavesCurrentlyNonEmpty = 0, numLemmaAlreadyExisted = 0; - for(typeof(leaves.begin()) it = leaves.begin(); it != leaves.end(); ++it) { + for(std::set::iterator it = leaves.begin(); it != leaves.end(); ++it) { bool generateLemma = true; Node emptySet = nm->mkConst(EmptySet(nm->toType((*it).getType()))); @@ -2447,7 +2471,7 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { NodeManager* nm = NodeManager::currentNM(); // Introduce - for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin(); + for(CDNodeSet::const_iterator it = d_cardTerms.begin(); it != d_cardTerms.end(); ++it) { for(eq::EqClassIterator j(d_equalityEngine.getRepresentative((*it)[0]), &d_equalityEngine); @@ -2630,14 +2654,14 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { // merge_nodes(get_leaves(np.first), get_leaves(np.second), EQUAL(np.first, np.second)); merge_nodes(get_leaves(np.first), get_leaves(np.second), eqSoFar()); } - + if(d_newLemmaGenerated) { Trace("sets-card") << "[sets-card] New merge done. Returning." << std::endl; return; } leaves.clear(); - for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) { + for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { TNode v = *it; if(d_E.find(v) == d_E.end()) { leaves.insert(v); @@ -2657,23 +2681,28 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { } } + typedef std::set::const_iterator TNodeSetIterator; + // Elements being either equal or disequal [Members Arrangement rule] - Trace("sets-card") << "[sets-card] Processing elements equality/disequal to each other" << std::endl; - for(typeof(leaves.begin()) it = leaves.begin(); - it != leaves.end(); ++it) { - if(!d_equalityEngine.hasTerm(*it)) continue; + Trace("sets-card") + << "[sets-card] Processing elements equality/disequal to each other" + << std::endl; + for (TNodeSetIterator it = leaves.begin(); it != leaves.end(); ++it) { + if (!d_equalityEngine.hasTerm(*it)) continue; Node n = d_equalityEngine.getRepresentative(*it); Assert(n.getKind() == kind::EMPTYSET || leaves.find(n) != leaves.end()); - if(n != *it) continue; + if (n != *it) continue; const CDTNodeList* l = d_termInfoManager->getMembers(*it); std::set elems; - for(typeof(l->begin()) l_it = l->begin(); l_it != l->end(); ++l_it) { + for (CDTNodeList::const_iterator l_it = l->begin(); l_it != l->end(); ++l_it) { elems.insert(d_equalityEngine.getRepresentative(*l_it)); } - for(typeof(elems.begin()) e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) { - for(typeof(elems.begin()) e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) { - if(*e1_it == *e2_it) continue; - if(!d_equalityEngine.areDisequal(*e1_it, *e2_it, false)) { + for (TNodeSetIterator e1_it = elems.begin(); e1_it != elems.end(); + ++e1_it) { + for (TNodeSetIterator e2_it = elems.begin(); e2_it != elems.end(); + ++e2_it) { + if (*e1_it == *e2_it) continue; + if (!d_equalityEngine.areDisequal(*e1_it, *e2_it, false)) { Node lem = nm->mkNode(kind::EQUAL, *e1_it, *e2_it); lem = nm->mkNode(kind::OR, lem, nm->mkNode(kind::NOT, lem)); lemma(lem, SETS_LEMMA_GRAPH); @@ -2689,8 +2718,7 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { // Assert Lower bound Trace("sets-card") << "[sets-card] Processing assert lower bound" << std::endl; - for(typeof(leaves.begin()) it = leaves.begin(); - it != leaves.end(); ++it) { + for(TNodeSetIterator it = leaves.begin(); it != leaves.end(); ++it) { Trace("sets-cardlower") << "[sets-cardlower] Card Lower: " << *it << std::endl; Assert(d_equalityEngine.hasTerm(*it)); Node n = d_equalityEngine.getRepresentative(*it); @@ -2703,21 +2731,21 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { // if(n != *it) continue; const CDTNodeList* l = d_termInfoManager->getMembers(n); std::set elems; - for(typeof(l->begin()) l_it = l->begin(); l_it != l->end(); ++l_it) { + for(CDTNodeList::const_iterator l_it = l->begin(); l_it != l->end(); ++l_it) { elems.insert(d_equalityEngine.getRepresentative(*l_it)); } if(elems.size() == 0) continue; NodeBuilder<> nb(kind::OR); nb << ( nm->mkNode(kind::LEQ, nm->mkConst(Rational(elems.size())), nm->mkNode(kind::CARD, *it)) ); if(elems.size() > 1) { - for(typeof(elems.begin()) e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) { - for(typeof(elems.begin()) e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) { + for(TNodeSetIterator e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) { + for(TNodeSetIterator e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) { if(*e1_it == *e2_it) continue; nb << (nm->mkNode(kind::EQUAL, *e1_it, *e2_it)); } } } - for(typeof(elems.begin()) e_it = elems.begin(); e_it != elems.end(); ++e_it) { + for(TNodeSetIterator e_it = elems.begin(); e_it != elems.end(); ++e_it) { nb << nm->mkNode(kind::NOT, nm->mkNode(kind::MEMBER, *e_it, *it)); } Node lem = Node(nb); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index e14efd7a4..71a6d9b2d 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -144,7 +144,8 @@ private: public: CDNodeSet d_terms; private: - std::hash_map d_info; + typedef std::hash_map SetsTermInfoMap; + SetsTermInfoMap d_info; void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const; void pushToSettermPropagationQueue(TNode x, TNode S, bool polarity); @@ -249,7 +250,7 @@ private: bool d_cardEnabled; void enableCard(); void cardCreateEmptysetSkolem(TypeNode t); - + CDNodeSet d_cardTerms; std::set d_typesAdded; CDNodeSet d_processedCardTerms; -- 2.30.2