From 4de6452284ff546d67d7e483bd4cb9a9bc64d8e3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 26 Mar 2014 02:58:45 -0400 Subject: [PATCH] add construles, type_rules rm redundant, kinds cleanup --- src/theory/sets/kinds | 56 ++++++++------- src/theory/sets/theory_sets_private.cpp | 48 +++++++++---- src/theory/sets/theory_sets_private.h | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 14 ++-- src/theory/sets/theory_sets_type_rules.h | 71 +++++-------------- .../sets/mar2014/stacks0.hs.78.cvc4.smt2 | 1 + 6 files changed, 90 insertions(+), 102 deletions(-) create mode 100644 test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index e46f3a4f8..12f114fc0 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -4,24 +4,25 @@ # src/theory/builtin/kinds. # -theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h" +theory THEORY_SETS \ + ::CVC4::theory::sets::TheorySets \ + "theory/sets/theory_sets.h" typechecker "theory/sets/theory_sets_type_rules.h" -rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h" +rewriter ::CVC4::theory::sets::TheorySetsRewriter \ + "theory/sets/theory_sets_rewriter.h" properties parametric -properties check propagate #presolve postsolve +properties check propagate -# Theory content goes here. - -# constants... +# constants constant EMPTYSET \ ::CVC4::EmptySet \ ::CVC4::EmptySetHashFunction \ "util/emptyset.h" \ "empty set" -# types... -operator SET_TYPE 1 "set type" # the type +# the type +operator SET_TYPE 1 "set type" cardinality SET_TYPE \ "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \ "theory/sets/theory_sets_type_rules.h" @@ -33,24 +34,25 @@ enumerator SET_TYPE \ "::CVC4::theory::sets::SetEnumerator" \ "theory/sets/theory_sets_type_enumerator.h" -# operators... -operator UNION 2 "set union" -operator INTERSECTION 2 "set intersection" -operator SETMINUS 2 "set subtraction" -operator SUBSET 2 "subset" -operator MEMBER 2 "set membership" - -operator SET_SINGLETON 1 "singleton set" - -typerule UNION ::CVC4::theory::sets::SetUnionTypeRule -typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule -typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule -typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule -typerule MEMBER ::CVC4::theory::sets::SetMemberTypeRule -typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule -typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule - -construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule -construle UNION ::CVC4::theory::sets::SetConstTypeRule +# operators +operator UNION 2 "set union" +operator INTERSECTION 2 "set intersection" +operator SETMINUS 2 "set subtraction" +operator SUBSET 2 "subset" +operator MEMBER 2 "set membership" +operator SET_SINGLETON 1 "singleton set" + +typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule +typerule MEMBER ::CVC4::theory::sets::MemberTypeRule +typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule +typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule + +construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule endtheory diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 70b757f0c..f487e1566 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -419,15 +419,14 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements } - -void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const { +bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const { Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): " << std::endl; Assert(S.getType().isSet()); - Elements emptySetOfElements; + const Elements emptySetOfElements; const Elements& saved = d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ? emptySetOfElements : @@ -438,9 +437,18 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, if(S.getNumChildren() == 2) { - Elements cur, left, right; - left = settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second; - right = settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second; + Elements cur; + + const Elements& left = + d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ? + emptySetOfElements : + settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second; + + const Elements& right = + d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ? + emptySetOfElements : + settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second; + switch(S.getKind()) { case kind::UNION: if(left.size() >= right.size()) { @@ -466,16 +474,18 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, Debug("sets-model") << " }" << std::endl; if(saved != cur) { - Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved " + Debug("sets-model") << "[sets-model] *** ERROR *** cur != saved " << std::endl; - Debug("sets-model") << "[sets-model] FYI: " - << " [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", " - << " [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", " - << " [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n"; + Debug("sets-model") + << "[sets-model] FYI: " + << " [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", " + << " [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", " + << " [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n"; + return false; } - Assert( saved == cur ); } + return true; } Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const @@ -516,6 +526,15 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) TNode x = d_equalityEngine.getRepresentative(n[0]); TNode S = d_equalityEngine.getRepresentative(n[1]); settermElementsMap[S].insert(x); + if(Debug.isOn("sets-model-details")) { + vector explanation; + d_equalityEngine.explainPredicate(n, true, explanation); + Debug("sets-model-details") + << "[sets-model-details] > node: " << n << ", explanation:" << std::endl; + BOOST_FOREACH(TNode m, explanation) { + Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; + } + } } } @@ -560,11 +579,14 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) } #ifdef CVC4_ASSERTIONS + bool checkPassed = true; BOOST_FOREACH(TNode term, terms) { if( term.getType().isSet() ) { - checkModel(settermElementsMap, term); + checkPassed &= checkModel(settermElementsMap, term); } } + Assert( checkPassed, + "THEORY_SETS check-model failed. Run with -d sets-model for details." ); #endif } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 62274e1ce..9576384bb 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -165,7 +165,7 @@ private: typedef std::hash_map SettermElementsMap; const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const; Node elementsToShape(Elements elements, TypeNode setType) const; - void checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; + bool checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; };/* class TheorySetsPrivate */ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 109d8bb0e..328592abb 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -68,13 +68,13 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { switch(kind) { case kind::MEMBER: { - if(!node[0].isConst() || !node[1].isConst()) - break; - - // both are constants - TNode S = preRewrite(node[1]).node; - bool isMember = checkConstantMembership(node[0], S); - return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember)); + if(node[0].isConst() && node[1].isConst()) { + // both are constants + TNode S = preRewrite(node[1]).node; + bool isMember = checkConstantMembership(node[0], S); + return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember)); + } + break; }//kind::MEMBER case kind::SUBSET: { diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index aee2c92b5..3b2acd956 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -44,62 +44,34 @@ public: };/* class SetsTypeRule */ -// TODO: Union, Intersection and Setminus should be combined to one check -struct SetUnionTypeRule { +struct SetsBinaryOperatorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - Assert(n.getKind() == kind::UNION); + Assert(n.getKind() == kind::UNION || + n.getKind() == kind::INTERSECTION || + n.getKind() == kind::SETMINUS); TypeNode setType = n[0].getType(check); if( check ) { if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "set union operating on non-set"); + throw TypeCheckingExceptionPrivate(n, "operator expects a set, first argument is not"); } TypeNode secondSetType = n[1].getType(check); if(secondSetType != setType) { - throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types"); + throw TypeCheckingExceptionPrivate(n, "operator expects two sets of the same type"); } } return setType; } -};/* struct SetUnionTypeRule */ -struct SetIntersectionTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - Assert(n.getKind() == kind::INTERSECTION); - TypeNode setType = n[0].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "set intersection operating on non-set"); - } - TypeNode secondSetType = n[1].getType(check); - if(secondSetType != setType) { - throw TypeCheckingExceptionPrivate(n, "set intersection operating on sets of different types"); - } - } - return setType; - } -};/* struct SetIntersectionTypeRule */ - -struct SetSetminusTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - Assert(n.getKind() == kind::SETMINUS); - TypeNode setType = n[0].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "set setminus operating on non-set"); - } - TypeNode secondSetType = n[1].getType(check); - if(secondSetType != setType) { - throw TypeCheckingExceptionPrivate(n, "set setminus operating on sets of different types"); - } - } - return setType; + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::UNION || + n.getKind() == kind::INTERSECTION || + n.getKind() == kind::SETMINUS); + return n[0].isConst() && n[1].isConst(); } -};/* struct SetSetminusTypeRule */ +};/* struct SetUnionTypeRule */ -struct SetSubsetTypeRule { +struct SubsetTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::SUBSET); @@ -117,7 +89,7 @@ struct SetSubsetTypeRule { } };/* struct SetSubsetTypeRule */ -struct SetMemberTypeRule { +struct MemberTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::MEMBER); @@ -141,25 +113,16 @@ struct SetSingletonTypeRule { Assert(n.getKind() == kind::SET_SINGLETON); return nodeManager->mkSetType(n[0].getType(check)); } -};/* struct SetInTypeRule */ -struct SetConstTypeRule { inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - switch(n.getKind()) { - case kind::SET_SINGLETON: - return n[0].isConst(); - case kind::UNION: - return n[0].isConst() && n[1].isConst(); - default: - Unhandled(); - } + Assert(n.getKind() == kind::SET_SINGLETON); + return n[0].isConst(); } -}; +};/* struct SetInTypeRule */ struct EmptySetTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - Assert(n.getKind() == kind::EMPTYSET); EmptySet emptySet = n.getConst(); Type setType = emptySet.getType(); diff --git a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 new file mode 100644 index 000000000..70c0057f9 --- /dev/null +++ b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 @@ -0,0 +1 @@ +; PLACEHOLDER: benchmark to be added -- 2.30.2