From: Kshitij Bansal Date: Thu, 3 Jul 2014 23:17:18 +0000 (-0400) Subject: improvements to sets sharing X-Git-Tag: cvc5-1.0.0~6649 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2482d287fe3ebcd78e6ebd9a4910d1646251b3fe;p=cvc5.git improvements to sets sharing * Add TheorySets::getEqualityStatus(TNode, TNode) * Add TheorySets::getModelValue(TNode) --- diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 220737d2e..c657796ee 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -335,7 +335,7 @@ TheoryArithPrivate::Statistics::Statistics() , d_unsatPivots("theory::arith::pivots::unsat") , d_unknownPivots("theory::arith::pivots::unkown") , d_solveIntModelsAttempts("theory::arith::z::solveInt::models::attempts", 0) - , d_solveIntModelsSuccessful("zzz::solveInt::models::successful", 0) + , d_solveIntModelsSuccessful("theory::arith::zzz::solveInt::models::successful", 0) , d_mipTimer("theory::arith::z::approx::mip::timer") , d_lpTimer("theory::arith::z::approx::lp::timer") , d_mipProofsAttempted("theory::arith::z::mip::proofs::attempted", 0) diff --git a/src/theory/sets/options b/src/theory/sets/options index 1c95e78e4..7cb3eb677 100644 --- a/src/theory/sets/options +++ b/src/theory/sets/options @@ -11,4 +11,7 @@ option setsPropagate --sets-propagate bool :default true option setsEagerLemmas --sets-eager-lemmas bool :default true add lemmas even at regular effort +option setsCare1 --sets-care1 bool :default false + generate one lemma at a time for care graph + endmodule diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index b59beac8d..faba2aab1 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -54,6 +54,14 @@ Node TheorySets::explain(TNode node) { return d_internal->explain(node); } +EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) { + return d_internal->getEqualityStatus(a, b); +} + +Node TheorySets::getModelValue(TNode node) { + return d_internal->getModelValue(node); +} + void TheorySets::preRegisterTerm(TNode node) { d_internal->preRegisterTerm(node); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a16832389..6136fc8f8 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -58,6 +58,10 @@ public: Node explain(TNode); + EqualityStatus getEqualityStatus(TNode a, TNode b); + + Node getModelValue(TNode); + std::string identify() const { return "THEORY_SETS"; } void preRegisterTerm(TNode node); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 592b4bc37..a8f6dcc38 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -27,6 +27,8 @@ #include "util/emptyset.h" #include "util/result.h" +#include "util/partitions.h" + using namespace std; using namespace CVC4::expr::pattern; @@ -420,29 +422,213 @@ void TheorySetsPrivate::addSharedTerm(TNode n) { void TheorySetsPrivate::computeCareGraph() { Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl; - for (unsigned i = 0; i < d_external.d_sharedTerms.size(); ++ i) { + + // dump our understanding of assertions + if(Trace.isOn("sets-assertions") + || Trace.isOn("sets-care-dump")) + { + std::string tag = "sets-assertions"; + 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; + static std::map numbering; + static int number = 0; + + for (unsigned i = 0; it != it_end; ++ it, ++i) { + TNode ass = (*it).assertion; + Trace("sets-care-dump") << AssertCommand(ass.toExpr()) << endl; + bool polarity = ass.getKind() != kind::NOT; + ass = polarity ? ass : ass[0]; + Assert( ass.getNumChildren() == 2); + TNode left = d_equalityEngine.getRepresentative(ass[0]); + TNode right = d_equalityEngine.getRepresentative(ass[1]); + if(numbering[left] == 0) numbering[left] = ++number; + if(numbering[right] == 0) numbering[right] = ++number; + equalities[left].insert(ass[0]); + equalities[right].insert(ass[1]); + if(ass.getKind() == kind::EQUAL) { + if(polarity) { + Assert(left == right); + } else { + if(left > right) std::swap(left, right); + disequalities.insert(make_pair(left, right)); + } + } else if(ass.getKind() == kind::MEMBER) { + (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) { + Trace(tag) << " Eq class of t" << numbering[(*kt).first] << ": " << std::endl; + FORIT(jt, (*kt).second) { + TNode S = (*jt); + if( S.getKind() != kind::UNION && S.getKind() != kind::INTERSECTION && S.getKind() != kind::SETMINUS) { + Trace(tag) << " " << *jt << ((*jt).getType().isSet() ? "\n": " "); + } else { + Trace(tag) << " "; + if(S[0].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[0])) == numbering.end()) { + Trace(tag) << S[0]; + } else { + Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[0])]; + } + Trace(tag) << " " << (S.getKind() == kind::UNION ? "|" : (S.getKind() == kind::INTERSECTION ? "&" : "-")) << " "; + if(S[1].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[1])) == numbering.end()) { + Trace(tag) << S[1]; + } else { + Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[1])]; + } + Trace(tag) << std::endl; + } + } + Trace(tag) << std::endl; + } + FORIT(kt, disequalities) Trace(tag) << "NOT(t"< 0) { + Trace(tag) << "IN t" << numbering[(*kt).first] << ": "; + FORIT(jt, (*kt).second.first) { + TNode x = (*jt); + if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) { + Trace(tag) << x; + } else { + Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", "; + } + } + Trace(tag) << std::endl; + } + if( (*kt).second.second.size() > 0) { + Trace(tag) << "NOT IN t" << numbering[(*kt).first] << ": "; + FORIT(jt, (*kt).second.second) { + TNode x = (*jt); + if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) { + Trace(tag) << x; + } else { + Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", "; + } + } + Trace(tag) << std::endl; + } + } + Trace(tag) << std::endl; + + } + + std::map > careGraphVertices; + + for (unsigned i = d_ccg_i; i < d_external.d_sharedTerms.size(); ++ i) { TNode a = d_external.d_sharedTerms[i]; TypeNode aType = a.getType(); - for (unsigned j = i + 1; j < d_external.d_sharedTerms.size(); ++ j) { + // if(a.getType().isSet()) { + // int sizeMem = d_termInfoManager->getMembers(d_equalityEngine.getRepresentative(a))->size(); + // int sizeNonMem = d_termInfoManager->getNonMembers(d_equalityEngine.getRepresentative(a))->size(); + // Debug("sets-care") << "[sets-care] " << a << " : " << sizeMem << " " << sizeNonMem << std::endl; + // if(sizeMem == 0 && sizeNonMem == 0) continue; + // } + unsigned j_st; + if(i == d_ccg_i) j_st = d_ccg_j + 1; + else j_st = i + 1; + for (unsigned j = j_st; j < d_external.d_sharedTerms.size(); ++ j) { TNode b = d_external.d_sharedTerms[j]; if (b.getType() != aType) { // We don't care about the terms of different types continue; } + // if(b.getType().isSet()) { + // int sizeMem = d_termInfoManager->getMembers(d_equalityEngine.getRepresentative(b))->size(); + // int sizeNonMem = d_termInfoManager->getNonMembers(d_equalityEngine.getRepresentative(b))->size(); + // Debug("sets-care") << "[sets-care] " << a << " : " << sizeMem << " " << sizeNonMem << std::endl; + // if(sizeMem == 0 && sizeNonMem == 0) continue; + // } switch (d_external.d_valuation.getEqualityStatus(a, b)) { case EQUALITY_TRUE_AND_PROPAGATED: + // If we know about it, we should have propagated it, so we can skip + Trace("sets-care") << "[sets-care] Know: " << EQUAL(a, b) << std::endl; + break; case EQUALITY_FALSE_AND_PROPAGATED: // If we know about it, we should have propagated it, so we can skip + Trace("sets-care") << "[sets-care] Know: " << NOT(EQUAL(a, b)) << std::endl; break; - default: + case EQUALITY_FALSE: + case EQUALITY_TRUE: + Assert(false, "ERROR: Equality status true/false but not propagated (sets care graph computation)."); + break; + case EQUALITY_TRUE_IN_MODEL: + d_external.addCarePair(a, b); + case EQUALITY_FALSE_IN_MODEL: + if(Trace.isOn("sets-care-performance-test")) { + // TODO: delete these lines, only for performance testing for now + d_external.addCarePair(a, b); + } + break; + case EQUALITY_UNKNOWN: // Let's split on it d_external.addCarePair(a, b); + if(options::setsCare1()) { + d_ccg_i = i; + d_ccg_j = j; + return; + } + if(Trace.isOn("sets-care-dump")) { + careGraphVertices[a.getType()].insert(a); + careGraphVertices[a.getType()].insert(b); + } break; + default: + Unreachable(); } } } + + if(Trace.isOn("sets-care-dump")) { + FORIT(it, careGraphVertices) { + // Trace("sets-care-dump") << "For " << (*it).first << ": " << std::endl; + std::set& S = (*it).second; + for(util::partition::iterator subsets(S.size()); + !subsets.isFinished(); ++subsets) { + Trace("sets-care-dump") << ";---split---" << std::endl; + Trace("sets-care-dump") << ";"; + for(unsigned i = 0; i < S.size(); ++i) Trace("sets-care-dump") << subsets.get(i); + Trace("sets-care-dump") << std::endl; + int j = 0; + FORIT(jt, (*it).second) { + int k = 0; + FORIT(kt, (*it).second) { + if(j == k) continue; + Node n = EQUAL( (*jt), (*kt) ); + if(!subsets.equal(j, k)) n = NOT(n); + Trace("sets-care-dump") << AssertCommand(n.toExpr()) << std::endl; + ++k; + } + ++j; + } + } + } + Trace("sets-care-dump") << ";---split---" << std::endl; +#undef FORIT + } } +EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { + Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)); + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b, false)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + if( d_external.d_valuation.getModelValue(a) == d_external.d_valuation.getModelValue(b) ) { + // Ther term are true in current model + return EQUALITY_TRUE_IN_MODEL; + } + return EQUALITY_FALSE_IN_MODEL; + // } + // //TODO: can we be more precise sometimes? + // return EQUALITY_UNKNOWN; +} /******************** Model generation ********************/ /******************** Model generation ********************/ @@ -578,6 +764,21 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con return cur; } } +Node TheorySetsPrivate::elementsToShape(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(); + Node cur = SINGLETON(*it); + while( ++it != elements.end() ) { + cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it)); + } + return cur; + } +} void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) { @@ -684,6 +885,11 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) #endif } +Node TheorySetsPrivate::getModelValue(TNode n) +{ + CodeTimer codeTimer(d_statistics.d_getModelValueTime); + return d_termInfoManager->getModelValue(n); +} /********************** Helper functions ***************************/ /********************** Helper functions ***************************/ @@ -730,14 +936,17 @@ Node mkAnd(const std::vector& conjunctions) { TheorySetsPrivate::Statistics::Statistics() : - d_checkTime("theory::sets::time") { - + d_checkTime("theory::sets::time") + , d_getModelValueTime("theory::sets::getModelValueTime") +{ StatisticsRegistry::registerStat(&d_checkTime); + StatisticsRegistry::registerStat(&d_getModelValueTime); } TheorySetsPrivate::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_checkTime); + StatisticsRegistry::unregisterStat(&d_getModelValueTime); } @@ -876,6 +1085,9 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_pending(c), d_pendingDisequal(c), d_pendingEverInserted(u), + d_modelCache(c), + d_ccg_i(c), + d_ccg_j(c), d_scrutinize(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); @@ -1106,6 +1318,8 @@ void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) { d_info[S]->addToElementList(x, polarity); d_info[x]->addToSetList(S, polarity); + + d_theory.d_modelCache.clear(); } const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) { @@ -1259,8 +1473,35 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { (*itb).second->setsContainingThisElement ); mergeLists( (*ita).second->setsNotContainingThisElement, (*itb).second->setsNotContainingThisElement ); + + d_theory.d_modelCache.clear(); } +Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) +{ + Assert(n.getType().isSet()); + set elements, 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()) { + return (*it).second; + } + const CDTNodeList* l = getMembers(S); + for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + TNode n = *it; + elements.insert(d_eqEngine->getRepresentative(n)); + } + BOOST_FOREACH(TNode e, elements) { + if(e.isConst()) { + elements_const.insert(e); + } else { + elements_const.insert(d_theory.d_external.d_valuation.getModelValue(e)); + } + } + Node v = d_theory.elementsToShape(elements_const, n.getType()); + d_theory.d_modelCache[n] = v; + return v; +} }/* CVC4::theory::sets namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 78a415529..b293c63e6 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -60,6 +60,10 @@ public: Node explain(TNode); + EqualityStatus getEqualityStatus(TNode a, TNode b); + + Node getModelValue(TNode); + void preRegisterTerm(TNode node); void propagate(Theory::Effort) { /* we don't depend on this call */ } @@ -70,6 +74,7 @@ private: class Statistics { public: TimerStat d_checkTime; + TimerStat d_getModelValueTime; Statistics(); ~Statistics(); @@ -123,6 +128,7 @@ private: void notifyMembership(TNode fact); const CDTNodeList* getParents(TNode x); const CDTNodeList* getMembers(TNode S); + Node getModelValue(TNode n); const CDTNodeList* getNonMembers(TNode S); void addTerm(TNode n); void mergeTerms(TNode a, TNode b); @@ -174,8 +180,15 @@ private: typedef std::hash_map SettermElementsMap; const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const; Node elementsToShape(Elements elements, TypeNode setType) const; + Node elementsToShape(std::set elements, TypeNode setType) const; bool checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; + context::CDHashMap d_modelCache; + + + // sharing related + context::CDO d_ccg_i, d_ccg_j; + // more debugging stuff friend class TheorySetsScrutinize; TheorySetsScrutinize* d_scrutinize; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index eb270202a..6754bbb9e 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -100,7 +100,7 @@ struct MemberTypeRule { } TypeNode elementType = n[0].getType(check); if(elementType != setType.getSetElementType()) { - throw TypeCheckingExceptionPrivate(n, "set in operating on sets of different types"); + throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); } } return nodeManager->booleanType(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 53a529325..19409faf7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -155,7 +155,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_sharedTermsVisitor(d_sharedTerms), d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_bvToBoolPreprocessor(), - d_arithSubstitutionsAdded("zzz::arith::substitutions", 0) + d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; @@ -453,7 +453,7 @@ void TheoryEngine::check(Theory::Effort effort) { void TheoryEngine::combineTheories() { - Debug("sharing") << "TheoryEngine::combineTheories()" << endl; + Trace("sharing") << "TheoryEngine::combineTheories()" << endl; TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime); @@ -471,7 +471,7 @@ void TheoryEngine::combineTheories() { // Call on each parametric theory to give us its care graph CVC4_FOR_EACH_THEORY; - Debug("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl; + Trace("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl; // Now add splitters for the ones we are interested in CareGraph::const_iterator care_it = careGraph.begin(); @@ -1393,17 +1393,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node); } - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. if(negated) { - // Can't we just get rid of passing around this 'negated' stuff? - // Is it that hard for the propEngine to figure that out itself? - // (I like the use of triple negation .) --K additionalLemmas[0] = additionalLemmas[0].notNode(); negated = false; } - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. // assert to decision engine if(!removable) { diff --git a/src/util/partitions.h b/src/util/partitions.h new file mode 100644 index 000000000..eaf29932b --- /dev/null +++ b/src/util/partitions.h @@ -0,0 +1,94 @@ +#include +#include + +namespace CVC4 { +namespace util { + +class partition +{ +public: + class iterator + { + public: + /** + * iterate over all partitions of [0, 1, ... n-1] (same as + * generating equivalence relations) + * + * corresponds to n-th bell number (A000110 in OEIS) + */ + iterator(unsigned n, bool first = true); + + unsigned size() const { return kappa.size(); } + + /** How many partitions does the current paritioning use */ + unsigned subsets() const { return M[size() - 1] + 1; } + + /** Which partition is 'i' in? Numbering starts with 0. */ + int get(int i) { return kappa[i]; } + + /** Are 'i' and 'j' in the same partition */ + bool equal(int i, int j) { return kappa[i] == kappa[j]; } + + /** go to next partitioning */ + iterator& operator++(); + + bool isFinished() { return d_finished; } + protected: + std::vector kappa, M; + bool d_finished; + }; +}; + +/** + Implementation from + https://www.cs.bgu.ac.il/~orlovm/papers/partitions-source.tar.gz + + Released in public domain by Michael Orlov , + according to the accompaning paper (Efficient Generation of Set + Partitions, Appendix A). + + --Kshitij Bansal, Tue Aug 5 15:57:20 EDT 2014 +*/ + +partition::iterator:: +iterator(unsigned n, bool first) + : kappa(n), M(n), d_finished(false) +{ + if (n <= 0) + throw std::invalid_argument + ("partition::iterator: n must be positive"); + + if (! first) + for (unsigned i = 1; i < n; ++i) { + kappa[i] = i; + M[i] = i; + } +} + +partition::iterator& +partition::iterator:: +operator++() +{ + const unsigned n = size(); + + for (unsigned i = n-1; i > 0; --i) + if (kappa[i] <= M[i-1]) { + ++kappa[i]; + + const unsigned new_max = std::max(M[i], kappa[i]); + M[i] = new_max; + for (unsigned j = i + 1; j < n; ++j) { + kappa[j] = 0; + M[j] = new_max; + } + + // integrityCheck(); + return *this; + } + + d_finished = true; + return *this; +} + +} +}