diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /src/theory/sets | |
parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/normal_form.h | 74 | ||||
-rw-r--r-- | src/theory/sets/scrutinize.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 301 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 7 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 10 |
5 files changed, 234 insertions, 164 deletions
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 6da7e9f8f..c1f05ae85 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -24,58 +24,64 @@ namespace theory { namespace sets { class NormalForm { -public: - - template<bool ref_count> - static Node elementsToSet(std::set<NodeTemplate<ref_count> > elements, TypeNode setType) - { + public: + template <bool ref_count> + static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements, + TypeNode setType) { + typedef typename std::set<NodeTemplate<ref_count> >::const_iterator + ElementsIterator; NodeManager* nm = NodeManager::currentNM(); - - if(elements.size() == 0) { + if (elements.size() == 0) { return nm->mkConst(EmptySet(nm->toType(setType))); } else { - typeof(elements.begin()) it = elements.begin(); + ElementsIterator it = elements.begin(); Node cur = nm->mkNode(kind::SINGLETON, *it); - while( ++it != elements.end() ) { - cur = nm->mkNode(kind::UNION, cur, - nm->mkNode(kind::SINGLETON, *it)); + while (++it != elements.end()) { + cur = nm->mkNode(kind::UNION, cur, nm->mkNode(kind::SINGLETON, *it)); } return cur; } } static bool checkNormalConstant(TNode n) { - Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" << std::endl; - if(n.getKind() == kind::EMPTYSET) { + Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" + << std::endl; + if (n.getKind() == kind::EMPTYSET) { return true; - } else if(n.getKind() == kind::SINGLETON) { + } else if (n.getKind() == kind::SINGLETON) { return n[0].isConst(); - } else if(n.getKind() == kind::UNION) { - - // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ... {BiggestNodeId}) + } else if (n.getKind() == kind::UNION) { + // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ... + // {BiggestNodeId}) // store BiggestNodeId in prvs - if(n[1].getKind() != kind::SINGLETON) return false; - if( !n[1][0].isConst() ) return false; - Debug("sets-checknormal") << "[sets-checknormal] frst element = " << n[1][0] << " " << n[1][0].getId() << std::endl; + if (n[1].getKind() != kind::SINGLETON) return false; + if (!n[1][0].isConst()) return false; + Debug("sets-checknormal") + << "[sets-checknormal] frst element = " << n[1][0] << " " + << n[1][0].getId() << std::endl; TNode prvs = n[1][0]; n = n[0]; // check intermediate nodes - while(n.getKind() == kind::UNION) { - if(n[1].getKind() != kind::SINGLETON) return false; - if( !n[1].isConst() ) return false; - Debug("sets-checknormal") << "[sets-checknormal] element = " << n[1][0] << " " << n[1][0].getId() << std::endl; - if( n[1][0] >= prvs ) return false; - TNode prvs = n[1][0]; - n = n[0]; + while (n.getKind() == kind::UNION) { + if (n[1].getKind() != kind::SINGLETON) return false; + if (!n[1].isConst()) return false; + Debug("sets-checknormal") + << "[sets-checknormal] element = " << n[1][0] << " " + << n[1][0].getId() << std::endl; + if (n[1][0] >= prvs) return false; + TNode prvs = n[1][0]; + n = n[0]; } // check SmallestNodeID is smallest - if(n.getKind() != kind::SINGLETON) return false; - if( !n[0].isConst() ) return false; - Debug("sets-checknormal") << "[sets-checknormal] lst element = " << n[0] << " " << n[0].getId() << std::endl; - if( n[0] >= prvs ) return false; + if (n.getKind() != kind::SINGLETON) return false; + if (!n[0].isConst()) return false; + Debug("sets-checknormal") + << "[sets-checknormal] lst element = " << n[0] << " " + << n[0].getId() << std::endl; + if (n[0] >= prvs) return false; // we made it return true; @@ -88,10 +94,10 @@ public: static std::set<Node> getElementsFromNormalConstant(TNode n) { Assert(n.isConst()); std::set<Node> ret; - if(n.getKind() == kind::EMPTYSET) { + if (n.getKind() == kind::EMPTYSET) { return ret; } - while(n.getKind() == kind::UNION) { + while (n.getKind() == kind::UNION) { Assert(n[1].getKind() == kind::SINGLETON); ret.insert(ret.begin(), n[1][0]); n = n[0]; @@ -100,9 +106,7 @@ public: ret.insert(n[0]); return ret; } - }; - } } } diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h index 2ada4a3ce..88f6001b9 100644 --- a/src/theory/sets/scrutinize.h +++ b/src/theory/sets/scrutinize.h @@ -17,8 +17,6 @@ #pragma once -#include <boost/foreach.hpp> - #include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" @@ -55,7 +53,8 @@ public: } } bool checkPassed = true; - BOOST_FOREACH(TNode term, terms) { + for (std::set<Node>::const_iterator it = terms.begin(); it != terms.end(); it++){ + TNode term = *it; if( term.getType().isSet() ) { checkPassed &= d_theory->checkModel(settermElementsMap, term); } @@ -72,4 +71,3 @@ public: }/* CVC4::theory::sets namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index aec2c119c..e996cb215 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -218,7 +218,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, @@ -226,7 +226,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, @@ -255,7 +255,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; @@ -475,9 +475,15 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end(); - std::map<TNode, std::set<TNode> > equalities; - std::set< pair<TNode, TNode> > disequalities; - std::map<TNode, std::pair<std::set<TNode>, std::set<TNode> > > members; + typedef std::set<TNode> TNodeSet; + + typedef std::map<TNode, TNodeSet > EqualityMap; + EqualityMap equalities; + + typedef std::set< std::pair<TNode, TNode> > TNodePairSet; + TNodePairSet disequalities; + typedef std::map<TNode, std::pair<TNodeSet, TNodeSet > > MemberMap; + MemberMap members; static std::map<TNode, int> numbering; static int number = 0; @@ -504,10 +510,11 @@ 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) { + 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) { + + 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": " "); @@ -529,11 +536,17 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const } Trace(tag) << std::endl; } - FORIT(kt, disequalities) Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl; - FORIT(kt, members) { - if( (*kt).second.first.size() > 0) { - Trace(tag) << "IN t" << numbering[(*kt).first] << ": "; - FORIT(jt, (*kt).second.first) { + for(TNodePairSet::const_iterator kt=disequalities.begin(); kt != disequalities.end(); ++kt){ + Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl; + } + for(MemberMap::const_iterator kt=members.begin(); kt != members.end(); ++kt) { + const TNode& kt_key = (*kt).first; + const TNodeSet& kt_in_set = (*kt).second.first; + const TNodeSet& kt_out_set = (*kt).second.first; + if( kt_in_set.size() > 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 << ", "; @@ -543,9 +556,9 @@ 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] << ": "; + 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 << ", "; @@ -557,7 +570,6 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const } } Trace(tag) << std::endl; -#undef FORIT } void TheorySetsPrivate::computeCareGraph() { @@ -871,14 +883,15 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con return cur; } } -Node TheorySetsPrivate::elementsToShape(set<Node> elements, TypeNode setType) const + +Node TheorySetsPrivate::elementsToShape(std::set<Node> elements, TypeNode setType) const { NodeManager* nm = NodeManager::currentNM(); if(elements.size() == 0) { return nm->mkConst<EmptySet>(EmptySet(nm->toType(setType))); } else { - typeof(elements.begin()) it = elements.begin(); + std::set<Node>::const_iterator it = elements.begin(); Node cur = SINGLETON(*it); while( ++it != elements.end() ) { cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it)); @@ -892,13 +905,13 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) Trace("sets-model") << "[sets-model] collectModelInfo(..., fullModel=" << (fullModel ? "true)" : "false)") << std::endl; - set<Node> terms; + std::set<Node> 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) @@ -915,7 +928,8 @@ 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) { + print_graph(true); + 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; @@ -1005,7 +1019,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()); @@ -1102,7 +1116,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions) { if (t.getKind() == kind::AND) { for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { - Assert((*child_it).getKind() != kind::AND); + // Assert((*child_it).getKind() != kind::AND); all.insert(*child_it); } } @@ -1311,15 +1325,20 @@ Node TheorySetsPrivate::getLemma() { Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet()); TypeNode elementType = n[0].getType().getSetElementType(); - Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); - Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); - - if(n[0].getKind() == kind::EMPTYSET) { - lemma = OR(n, l2); - } else if(n[1].getKind() == kind::EMPTYSET) { - lemma = OR(n, l1); - } else { - lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); + // { x } != { y } => x != y + if( n[0].getKind()==kind::SINGLETON && n[1].getKind()==kind::SINGLETON ){ + lemma = OR(n, NodeManager::currentNM()->mkNode( elementType.isBoolean() ? kind::IFF : kind::EQUAL, n[0][0], n[1][0] ).negate() ); + }else{ + Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); + Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); + + if(n[0].getKind() == kind::EMPTYSET) { + lemma = OR(n, l2); + } else if(n[1].getKind() == kind::EMPTYSET) { + lemma = OR(n, l1); + } else { + lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); + } } } @@ -1412,7 +1431,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 ) { @@ -1496,7 +1515,11 @@ Node TheorySetsPrivate::explain(TNode literal) Unhandled(); } - return mkAnd(assumptions); + if(assumptions.size()) { + return mkAnd(assumptions); + } else { + return d_trueNode; + } } bool TheorySetsPrivate::lemma(Node n, SetsLemmaTag t) @@ -1568,14 +1591,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) << ", "; } @@ -1672,18 +1695,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; } } @@ -1744,14 +1767,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 ) ); } } @@ -1782,7 +1805,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 @@ -1850,8 +1873,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()); @@ -1879,29 +1902,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<Node> elements, elements_const; + std::set<Node> elements; + std::set<Node> 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<Node, Node, NodeHashFunction>::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<Node>::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); } } @@ -1910,9 +1937,6 @@ Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) return v; } - - - /********************** Cardinality ***************************/ /********************** Cardinality ***************************/ /********************** Cardinality ***************************/ @@ -1927,7 +1951,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) { @@ -1944,7 +1968,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)); } @@ -1971,9 +1995,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<std::pair<Node, Node>, 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; @@ -1988,7 +2013,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); @@ -2000,7 +2025,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); @@ -2017,32 +2042,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<TNode, std::set<TNode> >::const_iterator it = edgesFd.begin(); + it != edgesFd.end(); ++it) { + Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) + << std::endl; + for (std::set<TNode>::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<TNode, std::set<TNode> >::const_iterator it = edgesBk.begin(); + it != edgesBk.end(); ++it) { + Debug("sets-card-graph") << "[sets-card-graph] " << (it->first) + << std::endl; + for (std::set<TNode>::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() ) { @@ -2247,7 +2274,7 @@ std::set<TNode> TheorySetsPrivate::get_leaves(Node vertex1, Node vertex2, Node v Node TheorySetsPrivate::eqemptySoFar() { std::vector<Node> 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))); @@ -2391,11 +2418,12 @@ void TheorySetsPrivate::merge_nodes(std::set<TNode> leaves1, std::set<TNode> lea } -void TheorySetsPrivate::print_graph() { +void TheorySetsPrivate::print_graph(bool printmodel) { + NodeManager* nm = NodeManager::currentNM(); 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 << " : "; @@ -2414,15 +2442,40 @@ 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; + + std::ostringstream v_oss; + v_oss << v; + if(printmodel) + { + Node n = nm->mkNode(kind::CARD, v); + if((Rewriter::rewrite(n)).isConst()) { + v_oss << " " << (Rewriter::rewrite(n)); + } else { + v_oss << " " << d_external.d_valuation.getModelValue(n); + } + } + if(d_E.find(v) != d_E.end()) { BOOST_FOREACH(TNode w, d_E[v].get()) { + + std::ostringstream w_oss; + w_oss << w; + if(printmodel) { + Node n = nm->mkNode(kind::CARD, w); + if((Rewriter::rewrite(n)).isConst()) { + w_oss << " " << (Rewriter::rewrite(n)); + } else { + w_oss << " " << d_external.d_valuation.getModelValue(n); + } + } + //oss << v.getId() << " -> " << w.getId() << "; "; - oss << "\"" << v << "\" -> \"" << w << "\"; "; + oss << "\"" << v_oss.str() << "\" -> \"" << w_oss.str() << "\"; "; } } else { - oss << "\"" << v << "\";"; + oss << "\"" << v_oss.str() << "\";"; } } oss << "}"; @@ -2448,7 +2501,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); @@ -2465,7 +2518,7 @@ void TheorySetsPrivate::guessLeavesEmptyLemmas() { numLeavesCurrentlyNonEmpty = 0, numLemmaAlreadyExisted = 0; - for(typeof(leaves.begin()) it = leaves.begin(); it != leaves.end(); ++it) { + for(std::set<TNode>::iterator it = leaves.begin(); it != leaves.end(); ++it) { bool generateLemma = true; Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType((*it).getType()))); @@ -2526,8 +2579,16 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { NodeManager* nm = NodeManager::currentNM(); + if(options::setsGuessEmpty() == 0) { + Trace("sets-guess-empty") << "[sets-guess-empty] Generating lemmas before introduce." << std::endl; + guessLeavesEmptyLemmas(); + if(d_newLemmaGenerated) { + return; + } + } + // 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); @@ -2710,14 +2771,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); @@ -2737,23 +2798,28 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { } } + typedef std::set<TNode>::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<TNode> 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); @@ -2769,8 +2835,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); @@ -2783,21 +2848,21 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { // if(n != *it) continue; const CDTNodeList* l = d_termInfoManager->getMembers(n); std::set<TNode> 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 217432670..3ed608b90 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -146,7 +146,8 @@ private: public: CDNodeSet d_terms; private: - std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info; + typedef std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> SetsTermInfoMap; + SetsTermInfoMap d_info; void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const; void pushToSettermPropagationQueue(TNode x, TNode S, bool polarity); @@ -252,7 +253,7 @@ private: bool d_cardEnabled; void enableCard(); void cardCreateEmptysetSkolem(TypeNode t); - + CDNodeSet d_cardTerms; std::set<TypeNode> d_typesAdded; CDNodeSet d_processedCardTerms; @@ -282,7 +283,7 @@ private: std::set<TNode> get_leaves(Node vertex1, Node vertex2); std::set<TNode> get_leaves(Node vertex1, Node vertex2, Node vertex3); std::set<TNode> non_empty(std::set<TNode> vertices); - void print_graph(); + void print_graph(bool printmodel=false); context::CDQueue < std::pair<TNode, TNode> > d_graphMergesPending; context::CDList<Node> d_allSetEqualitiesSoFar; Node eqSoFar(); diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 40863b0f2..f2d6bae68 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -153,14 +153,16 @@ public: } while (d_constituentVec.size() < d_index) { - TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back()); - ++(*d_newEnumerator); - if( (*d_newEnumerator).isFinished() ) { + TypeEnumerator* newEnumerator = + new TypeEnumerator(*d_constituentVec.back()); + ++(*newEnumerator); + if (newEnumerator->isFinished()) { Trace("set-type-enum") << "operator++ finished!" << std::endl; + delete newEnumerator; d_finished = true; return *this; } - d_constituentVec.push_back(d_newEnumerator); + d_constituentVec.push_back(newEnumerator); } Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl; |