From 647c6045788cd586c4534e0b63744bff4dd2f1ef Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 16 May 2014 18:18:35 -0400 Subject: sets: fix a bug in model building, another in handling set of sets --- src/theory/sets/theory_sets_private.cpp | 43 +++++++++++++++++++++++++++++--- src/theory/sets/theory_sets_private.h | 2 ++ src/theory/sets/theory_sets_rewriter.cpp | 8 ++++-- src/theory/sets/theory_sets_rewriter.h | 1 - src/theory/theory_model.cpp | 4 +-- 5 files changed, 49 insertions(+), 9 deletions(-) (limited to 'src/theory') diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 9d00cde7b..af96b50d0 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -190,6 +190,29 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt) return; } + /** + * Disequality propagation if element type is set + */ + if(x.getType().isSet()) { + if(polarity) { + const CDTNodeList* l = d_termInfoManager->getNonMembers(S); + for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + TNode n = *it; + learnLiteral( /* atom = */ EQUAL(x, n), + /* polarity = */ false, + /* reason = */ AND( MEMBER(x, S), NOT( MEMBER(n, S)) ) ); + } + } else { + const CDTNodeList* l = d_termInfoManager->getMembers(S); + for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + TNode n = *it; + learnLiteral( /* atom = */ EQUAL(x, n), + /* polarity = */ false, + /* reason = */ AND( NOT(MEMBER(x, S)), MEMBER(n, S)) ); + } + } + } + for(; !j.isFinished(); ++j) { TNode S = (*j); Node cur_atom = MEMBER(x, S); @@ -227,7 +250,10 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S) Debug("sets-prop") << "[sets-prop] doSettermPropagation(" << x << ", " << S << std::endl; - Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType()); + Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType(), + ( std::string("types of S and x are ") + S.getType().toString() + + std::string(" and ") + x.getType().toString() + + std::string(" respectively") ).c_str() ); Node literal, left_literal, right_literal; @@ -416,7 +442,8 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements Unhandled(); } } else { - Assert(k == kind::VARIABLE || k == kind::APPLY_UF); + Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM, + (std::string("Expect variable or UF got ") + kindToString(k)).c_str() ); /* assign emptyset, which is default */ } @@ -598,6 +625,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) BOOST_FOREACH( TNode setterm, settermsModEq ) { Elements elements = getElements(setterm, settermElementsMap); Node shape = elementsToShape(elements, setterm.getType()); + shape = theory::Rewriter::rewrite(shape); m->assertEquality(shape, setterm, true); m->assertRepresentative(shape); } @@ -1042,6 +1070,14 @@ const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) { return d_info[x]->parents; } +const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) { + return d_info[S]->elementsInThisSet; +} + +const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) { + return d_info[S]->elementsNotInThisSet; +} + void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) { unsigned numChild = n.getNumChildren(); @@ -1052,8 +1088,7 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) { if(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION || - n.getKind() == kind::SETMINUS || - n.getKind() == kind::SET_SINGLETON) { + n.getKind() == kind::SETMINUS) { for(unsigned i = 0; i < numChild; ++i) { if(d_terms.contains(n[i])) { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 7e9d60905..9225bfbfd 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -118,6 +118,8 @@ private: ~TermInfoManager(); void notifyMembership(TNode fact); const CDTNodeList* getParents(TNode x); + const CDTNodeList* getMembers(TNode S); + const CDTNodeList* getNonMembers(TNode S); void addTerm(TNode n); void mergeTerms(TNode a, TNode b); }; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 328592abb..bcfbc46ae 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -201,12 +201,13 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette break; case kind::SET_SINGLETON: Assert(setterm[0].isConst()); - cur.insert(setterm[0]); + cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node); break; default: Unhandled(); } } + Debug("sets-rewrite-constant") << "[sets-rewrite-constant] "<< setterm << " " << setterm.getId() << std::endl; it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first; } @@ -246,7 +247,10 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { //rewrite set to normal form SettermElementsMap setTermElementsMap; // cache const Elements& elements = collectConstantElements(node, setTermElementsMap); - return RewriteResponse(REWRITE_DONE, elementsToNormalConstant(elements, node.getType())); + RewriteResponse response(REWRITE_DONE, elementsToNormalConstant(elements, node.getType())); + Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl + << "[sets-rewrite-constant] to " << response.node << std::endl; + return response; } return RewriteResponse(REWRITE_DONE, node); diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 715817508..6ce418e85 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -83,7 +83,6 @@ public: static inline void shutdown() { // nothing to do } - };/* class TheorySetsRewriter */ }/* CVC4::theory::sets namespace */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 203f116bb..6c0018c05 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -70,8 +70,8 @@ Node TheoryModel::getValue(TNode n) const { //normalize nn = Rewriter::rewrite(nn); } - Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): returning" - << nn << std::endl; + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl + << "[model-getvalue] returning " << nn << std::endl; return nn; } -- cgit v1.2.3