From: Kshitij Bansal Date: Fri, 16 May 2014 22:18:35 +0000 (-0400) Subject: sets: fix a bug in model building, another in handling set of sets X-Git-Tag: cvc5-1.0.0~6901^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=647c6045788cd586c4534e0b63744bff4dd2f1ef;p=cvc5.git sets: fix a bug in model building, another in handling set of sets --- 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; } diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 6d718553d..7f1f07461 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -31,6 +31,7 @@ TESTS = \ jan24/remove_check_free_31_6.smt2 \ sets-inter.smt2 \ sets-equal.smt2 \ + sets-disequal.smt2 \ union-2.smt2 \ jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \ jan27/ListConcat.hs.fqout.cvc4.177.smt2 \ @@ -69,10 +70,10 @@ EXTRA_DIST = $(TESTS) #TESTS += \ # error.cvc #endif -# -# and make sure to distribute it -#EXTRA_DIST += \ -# error.cvc + +# disabled tests, yet distribute +EXTRA_DIST += \ + setofsets-disequal.smt2 # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2 new file mode 100644 index 000000000..907e074fe --- /dev/null +++ b/test/regress/regress0/sets/setofsets-disequal.smt2 @@ -0,0 +1,64 @@ +; On a production build (as of 2014-05-16), takes several minutes +; to finish (2967466 decisions). + +(set-logic QF_BV_SETS) +(set-info :status unsat) + +(define-sort myset () (Set (Set (_ BitVec 1)))) +(declare-fun S () myset) + +; 0 elements +(assert (not (= S (as emptyset myset)))) + +; 1 element is S +(assert (not (= S (setenum (as emptyset (Set (_ BitVec 1))))))) +(assert (not (= S (setenum (setenum (_ bv0 1)) )))) +(assert (not (= S (setenum (setenum (_ bv1 1)) )))) +(assert (not (= S (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1))))))) + +; 2 elements in S +(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (setenum (_ bv0 1)))) ))) +(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (setenum (_ bv1 1))))))) +(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))))))) +(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))) + (setenum (setenum (_ bv0 1)))) ))) +(assert (not (= S (union (setenum (setenum (_ bv0 1))) + (setenum (setenum (_ bv1 1)))) ))) +(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))) + (setenum (setenum (_ bv1 1))))))) + +; 3 elements in S +(assert (not (= S (union (setenum (setenum (_ bv1 1))) + (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (setenum (_ bv0 1))))) ))) +(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))) + (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (setenum (_ bv1 1))))) ))) +(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))) + (union (setenum (setenum (_ bv0 1))) + (setenum (setenum (_ bv1 1))))) ))) +(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))) + (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (setenum (_ bv0 1))))) ))) + +; 4 elements in S +(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) + (setenum (_ bv1 1)))) + (union (setenum (setenum (_ bv1 1))) + (union (setenum (as emptyset (Set (_ BitVec 1)))) + (setenum (setenum (_ bv0 1)))))) ))) + +(check-sat) + +; if you delete any of the above assertions, you should get sat +; (get-model) diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress0/sets/sets-disequal.smt2 new file mode 100644 index 000000000..65f55f3a6 --- /dev/null +++ b/test/regress/regress0/sets/sets-disequal.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXIT: 0 +(set-logic QF_BV_SETS) +(declare-fun S1 () (Set (_ BitVec 1))) +(declare-fun S2 () (Set (_ BitVec 1))) +(declare-fun S3 () (Set (_ BitVec 1))) +(declare-fun S4 () (Set (_ BitVec 1))) +(assert (distinct S1 S2 S3 S4)) +(check-sat) +;(get-model) +(declare-fun S5 () (Set (_ BitVec 1))) +(assert (not (= S5 S1))) +(assert (not (= S5 S2))) +(assert (not (= S5 S3))) +(check-sat) +(assert (not (= S5 S4))) +(check-sat)