From 5021f49629637ff032c29cf2b2a7f55b5426897e Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 28 Aug 2014 14:29:00 -0400 Subject: [PATCH] sets stronger equality propagator --- src/theory/sets/options | 3 ++ src/theory/sets/theory_sets_private.cpp | 60 ++++++++++++++++++++++--- src/theory/sets/theory_sets_private.h | 5 ++- 3 files changed, 60 insertions(+), 8 deletions(-) diff --git a/src/theory/sets/options b/src/theory/sets/options index 7cb3eb677..ac040881a 100644 --- a/src/theory/sets/options +++ b/src/theory/sets/options @@ -14,4 +14,7 @@ option setsEagerLemmas --sets-eager-lemmas bool :default true option setsCare1 --sets-care1 bool :default false generate one lemma at a time for care graph +option setsPropFull --sets-prop-full bool :default false + agressive propagation + endmodule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 4125fd193..bfcb477cb 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -483,9 +483,9 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const FORIT(jt, (*kt).second.first) { TNode x = (*jt); if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) { - Trace(tag) << x; + Trace(tag) << x << ", "; } else { - Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", "; + Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", "; } } Trace(tag) << std::endl; @@ -495,9 +495,9 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const FORIT(jt, (*kt).second.second) { TNode x = (*jt); if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) { - Trace(tag) << x; + Trace(tag) << x << ", "; } else { - Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", "; + Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", "; } } Trace(tag) << std::endl; @@ -515,6 +515,8 @@ void TheorySetsPrivate::computeCareGraph() { dumpAssertionsHumanified(); } + CVC4_UNUSED unsigned edgesAddedCnt = 0; + unsigned i_st = 0; if(options::setsCare1()) { i_st = d_ccg_i; } for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) { @@ -546,6 +548,15 @@ void TheorySetsPrivate::computeCareGraph() { break; case EQUALITY_TRUE_IN_MODEL: d_external.addCarePair(a, b); + if(Trace.isOn("sharing")) { + ++edgesAddedCnt; + } + if(Debug.isOn("sets-care")) { + Debug("sets-care") << "[sets-care] Requesting split between" << a << " and " + << b << "." << std::endl << "[sets-care] " + << " Both current have value " + << d_external.d_valuation.getModelValue(a) << std::endl; + } case EQUALITY_FALSE_IN_MODEL: if(Trace.isOn("sets-care-performance-test")) { // TODO: delete these lines, only for performance testing for now @@ -566,6 +577,7 @@ void TheorySetsPrivate::computeCareGraph() { } } } + Trace("sharing") << "TheorySetsPrivate::computeCareGraph(): size = " << edgesAddedCnt << std::endl; } EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { @@ -1075,8 +1087,42 @@ TheorySetsPrivate::~TheorySetsPrivate() Assert(d_scrutinize != NULL); delete d_scrutinize; } -} +}/* TheorySetsPrivate::~TheorySetsPrivate() */ + +void TheorySetsPrivate::propagate(Theory::Effort effort) { + if(effort != Theory::EFFORT_FULL || !options::setsPropFull()) { + return; + } + + // build a model + Trace("sets-prop-full") << "[sets-prop-full] propagate(FULL_EFFORT)" << std::endl; + dumpAssertionsHumanified(); + + const CDNodeSet& terms = (d_termInfoManager->d_terms); + for(typeof(terms.begin()) it = terms.begin(); it != terms.end(); ++it) { + Node node = (*it); + Kind k = node.getKind(); + if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) { + + if(holds(MEMBER(node[0][0], node[1]))) { + Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[0][0], node[1]) + << " => " << EQUAL(node[1], node) << std::endl; + learnLiteral(EQUAL(node[1], node), MEMBER(node[0][0], node[1])); + } + } else if(k == kind::UNION && node[1].getKind() == kind::SINGLETON ) { + + if(holds(MEMBER(node[1][0], node[0]))) { + Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[1][0], node[0]) + << " => " << EQUAL(node[0], node) << std::endl; + learnLiteral(EQUAL(node[0], node), MEMBER(node[1][0], node[0])); + } + + } + } + + finishPropagation(); +} bool TheorySetsPrivate::propagate(TNode literal) { Debug("sets-prop") << " propagate(" << literal << ")" << std::endl; @@ -1094,13 +1140,14 @@ bool TheorySetsPrivate::propagate(TNode literal) { } return ok; -}/* TheorySetsPropagate::propagate(TNode) */ +}/* TheorySetsPrivate::propagate(TNode) */ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } + void TheorySetsPrivate::conflict(TNode a, TNode b) { if (a.getKind() == kind::CONST_BOOLEAN) { @@ -1139,6 +1186,7 @@ Node TheorySetsPrivate::explain(TNode literal) return mkAnd(assumptions); } + void TheorySetsPrivate::preRegisterTerm(TNode node) { Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")" diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 72c041d49..e5f160fda 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -66,7 +66,7 @@ public: void preRegisterTerm(TNode node); - void propagate(Theory::Effort) { /* we don't depend on this call */ } + void propagate(Theory::Effort); private: TheorySets& d_external; @@ -112,8 +112,9 @@ private: TheorySetsPrivate& d_theory; context::Context* d_context; eq::EqualityEngine* d_eqEngine; - + public: CDNodeSet d_terms; + private: std::hash_map d_info; void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const; -- 2.30.2