From 4de6452284ff546d67d7e483bd4cb9a9bc64d8e3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 26 Mar 2014 02:58:45 -0400 Subject: 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 ++++++---------------- .../regress0/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 -- cgit v1.2.3 From 5746fcdf2fe4c5472a817d18f1a536f6f4c31085 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 28 Mar 2014 18:37:02 -0400 Subject: get-antlr error on missing config.guess --- contrib/get-antlr-3.4 | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index 97cfe43af..74bce743e 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -26,6 +26,12 @@ function webget { } if [ -z "${MACHINE_TYPE}" ]; then + if ! [ -e config/config.guess ]; then + echo "$(basename $0): I need the file config/config.guess to tell MACHINE_TYPE" >&2 + echo "Try running ./autogen.sh, or set the MACHINE_TYPE environment variable." >&2 + exit 1 + fi + # get first nibble from config.guess (x86_64, i686, ...) MACHINE_TYPE=`config/config.guess | sed 's,-.*,,'` fi -- cgit v1.2.3 From feef8c2243734f8e6703164ee4d9a5980b7b1eb6 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 28 Mar 2014 18:33:38 -0400 Subject: rm old unused code --- src/theory/substitutions.cpp | 90 -------------------------------------------- src/theory/substitutions.h | 16 -------- 2 files changed, 106 deletions(-) diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index c4f06e396..9b9fc56d7 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -172,96 +172,6 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { } -/* We use subMap to simplify the left-hand sides of the current substitution map. If rewrite is true, - * we also apply the rewriter to the result. - * We want to maintain the invariant that all lhs are distinct from each other and from all rhs. - * If for some l -> r, l reduces to l', we try to add a new rule l' -> r. There are two cases - * where this fails - * (i) if l' is equal to some ll (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list - * (i) if l' is equalto some rr (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list - */ -/* -void SubstitutionMap::simplifyLHS(const SubstitutionMap& subMap, vector >& equalities, bool rewrite) -{ - Assert(d_worklist.empty()); - // First, apply subMap to every LHS in d_substitutions - NodeMap::iterator it = d_substitutions.begin(); - NodeMap::iterator it_end = d_substitutions.end(); - Node newLeft; - for(; it != it_end; ++ it) { - newLeft = subMap.apply((*it).first); - if (newLeft != (*it).first) { - if (rewrite) { - newLeft = Rewriter::rewrite(newLeft); - } - d_worklist.push_back(pair(newLeft, (*it).second)); - } - } - processWorklist(equalities, rewrite); - Assert(d_worklist.empty()); -} - - -void SubstitutionMap::simplifyLHS(TNode lhs, TNode rhs, vector >& equalities, bool rewrite) -{ - Assert(d_worklist.empty()); - d_worklist.push_back(pair(lhs,rhs)); - processWorklist(equalities, rewrite); - Assert(d_worklist.empty()); -} - - -void SubstitutionMap::processWorklist(vector >& equalities, bool rewrite) -{ - // Add each new rewrite rule, taking care not to invalidate invariants and looking - // for any new rewrite rules we can learn - Node newLeft, newRight; - while (!d_worklist.empty()) { - newLeft = d_worklist.back().first; - newRight = d_worklist.back().second; - d_worklist.pop_back(); - - NodeCache tempCache; - tempCache[newLeft] = newRight; - - Node newLeft2; - unsigned size = d_worklist.size(); - bool addThisRewrite = true; - NodeMap::iterator it = d_substitutions.begin(); - NodeMap::iterator it_end = d_substitutions.end(); - - for(; it != it_end; ++ it) { - - // Check for invariant violation. If new rewrite is redundant, do nothing - // Otherwise, add an equality to the output equalities - // In either case undo any work done by this rewrite - if (newLeft == (*it).first || newLeft == (*it).second) { - if ((*it).second != newRight) { - equalities.push_back(pair((*it).second, newRight)); - } - while (d_worklist.size() > size) { - d_worklist.pop_back(); - } - addThisRewrite = false; - break; - } - - newLeft2 = internalSubstituteOld((*it).first, tempCache); - if (newLeft2 != (*it).first) { - if (rewrite) { - newLeft2 = Rewriter::rewrite(newLeft2); - } - d_worklist.push_back(pair(newLeft2, (*it).second)); - } - } - if (addThisRewrite) { - d_substitutions[newLeft] = newRight; - d_cacheInvalidated = true; - } - } -} -*/ - void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a478a250..8572a6abd 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -95,10 +95,6 @@ private: */ CacheInvalidator d_cacheInvalidator; - // Helper list and method for simplifyLHS methods - // std::vector > d_worklist; - // void processWorklist(std::vector >& equalities, bool rewrite); - public: SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) : @@ -186,18 +182,6 @@ public: // Simplify right-hand sides of current map with lhs -> rhs void simplifyRHS(TNode lhs, TNode rhs); - /* - // Simplify left-hand sides of current map using the given substitutions - void simplifyLHS(const SubstitutionMap& subMap, - std::vector >& equalities, - bool rewrite = true); - - // Simplify left-hand sides of current map with lhs -> rhs and then add lhs -> rhs to the substitutions set - void simplifyLHS(TNode lhs, TNode rhs, - std::vector >& equalities, - bool rewrite = true); - */ - bool isSolvedForm() const { return d_solvedForm; } /** -- cgit v1.2.3