diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 23:44:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 23:44:00 +0000 |
commit | 97111ecb8681838f2d201420cda12ca9fc7184ed (patch) | |
tree | eee78a3ff75c1c9535b1db89ed273116a6ef3542 /src/util | |
parent | de164c9308f6461472b95c23aae68d9d9686d8ae (diff) |
Monday tasks:
* new "well-foundedness" type property (like cardinality) specified in
Theory kinds files; specifies well-foundedness and a ground term
* well-foundedness / finite checks in Datatypes now superseded by type
system isFinite(), isWellFounded(), mkGroundTerm().
* new "RecursionBreaker" template class, a convenient class that keeps
a "seen" trail without you having to pass it around (which is
difficult in cases of mutual recursion) of the idea of passing
around a "seen" trail
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/datatype.cpp | 303 | ||||
-rw-r--r-- | src/util/datatype.h | 78 | ||||
-rw-r--r-- | src/util/recursion_breaker.h | 133 |
4 files changed, 506 insertions, 9 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index a6ff0ea40..27b9e42d2 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -47,6 +47,7 @@ libutil_la_SOURCES = \ language.h \ language.cpp \ triple.h \ + recursion_breaker.h \ subrange_bound.h \ cardinality.h \ cardinality.cpp \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index afd5af703..20d63995f 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -23,7 +23,10 @@ #include "util/datatype.h" #include "expr/type.h" #include "expr/expr_manager.h" +#include "expr/expr_manager_scope.h" +#include "expr/node_manager.h" #include "expr/node.h" +#include "util/recursion_breaker.h" using namespace std; @@ -32,10 +35,20 @@ namespace CVC4 { namespace expr { namespace attr { struct DatatypeIndexTag {}; - } -} + struct DatatypeFiniteTag {}; + struct DatatypeWellFoundedTag {}; + struct DatatypeFiniteComputedTag {}; + struct DatatypeWellFoundedComputedTag {}; + struct DatatypeGroundTermTag {}; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr; +typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr; +typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr; +typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr; +typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> DatatypeWellFoundedComputedAttr; +typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr; const Datatype& Datatype::datatypeOf(Expr item) { TypeNode t = Node::fromExpr(item).getType(); @@ -73,6 +86,7 @@ void Datatype::resolve(ExprManager* em, "Datatype::resolve(): resolutions doesn't contain me!"); AssertArgument(placeholders.size() == replacements.size(), placeholders, "placeholders and replacements must be the same size"); + CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); DatatypeType self = (*resolutions.find(d_name)).second; AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; @@ -83,6 +97,7 @@ void Datatype::resolve(ExprManager* em, Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } + d_self = self; Assert(index == getNumConstructors()); } @@ -92,6 +107,166 @@ void Datatype::addConstructor(const Constructor& c) { d_constructors.push_back(c); } +Cardinality Datatype::getCardinality() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + return Cardinality::INTEGERS; + } + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c += (*i).getCardinality(); + } + return c; +} + +bool Datatype::isFinite() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + if(self.getAttribute(DatatypeFiniteComputedAttr())) { + return self.getAttribute(DatatypeFiniteAttr()); + } + + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! (*i).isFinite()) { + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), true); + return true; +} + +bool Datatype::isWellFounded() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + if(self.getAttribute(DatatypeWellFoundedComputedAttr())) { + return self.getAttribute(DatatypeWellFoundedAttr()); + } + + RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + // This *path* is cyclic, so may not be well-founded. The + // datatype itself might still be well-founded, though (we'll find + // the well-foundedness along another path). + return false; + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if((*i).isWellFounded()) { + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), true); + return true; + } + } + + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), false); + return false; +} + +Expr Datatype::mkGroundTerm() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr(); + if(!groundTerm.isNull()) { + Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl; + return groundTerm; + } else { + Debug("datatypes") << "\nNOT in cache: " << d_self << std::endl; + } + + // look for a nullary ctor and use that + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + // prefer the nullary constructor + if((*i).getNumArgs() == 0) { + groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor()); + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + Debug("datatypes") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl; + return groundTerm; + } + } + + // No ctors are nullary, but we can't just use the first ctor + // because that might recurse! In fact, since this datatype is + // well-founded by assumption, we know that at least one constructor + // doesn't contain a self-reference. We search for that one and use + // it to construct the ground term, as that is often a simpler + // ground term (e.g. in a tree datatype, something like "(leaf 0)" + // is simpler than "(node (leaf 0) (leaf 0))". + // + // Of course this check doesn't always work, if the self-reference + // is through other Datatypes (or other non-Datatype types), but it + // does simplify a common case. It requires a bit of extra work, + // but since we cache the results of these, it only happens once, + // ever, per Datatype. + // + // If the datatype is not actually well-founded, something below + // will throw an exception. + for(const_iterator i = begin(), i_end = end(); + i != i_end; + ++i) { + Constructor::const_iterator j = (*i).begin(), j_end = (*i).end(); + for(; j != j_end; ++j) { + SelectorType stype((*j).getSelector().getType()); + if(stype.getDomain() == stype.getRangeType()) { + Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl; + // the constructor contains a direct self-reference + break; + } + } + + if(j == j_end && (*i).isWellFounded()) { + groundTerm = (*i).mkGroundTerm(); + // Constructor::mkGroundTerm() doesn't ever return null when + // called from the outside. But in recursive invocations, it + // can: say you have dt = a(one:dt) | b(two:INT), and you ask + // the "a" constructor for a ground term. It asks "dt" for a + // ground term, which in turn asks the "a" constructor for a + // ground term! Thus, even though "a" is a well-founded + // constructor, it cannot construct a ground-term by itself. We + // have to skip past it, and we do that with a + // RecursionBreaker<> in Constructor::mkGroundTerm(). In the + // case of recursion, it returns null. + if(!groundTerm.isNull()) { + // we found a ground-term-constructing constructor! + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl; + return groundTerm; + } + } + } + // if we get all the way here, we aren't well-founded + CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!"); +} + +DatatypeType Datatype::getDatatypeType() const throw(AssertionException) { + CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + Assert(!d_self.isNull()); + return DatatypeType(d_self); +} + bool Datatype::operator==(const Datatype& other) const throw() { // two datatypes are == iff the name is the same and they have // exactly matching constructors (in the same order) @@ -279,15 +454,131 @@ std::string Datatype::Constructor::getName() const throw() { } Expr Datatype::Constructor::getConstructor() const { - CheckArgument(isResolved(), this, "this datatype constructor not yet resolved"); + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_constructor; } Expr Datatype::Constructor::getTester() const { - CheckArgument(isResolved(), this, "this datatype constructor not yet resolved"); + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_tester; } +Cardinality Datatype::Constructor::getCardinality() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + Cardinality c = 1; + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality(); + } + + return c; +} + +bool Datatype::Constructor::isFinite() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + if(self.getAttribute(DatatypeFiniteComputedAttr())) { + return self.getAttribute(DatatypeFiniteAttr()); + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), false); + return false; + } + } + + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), true); + return true; +} + +bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + if(self.getAttribute(DatatypeWellFoundedComputedAttr())) { + return self.getAttribute(DatatypeWellFoundedAttr()); + } + + RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + // This *path* is cyclic, sso may not be well-founded. The + // constructor itself might still be well-founded, though (we'll + // find the well-foundedness along another path). + return false; + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! SelectorType((*i).getSelector().getType()).getRangeType().isWellFounded()) { + /* FIXME - we can't cache a negative result here, because a + Datatype might tell us it's not well founded along this + *path*, due to recursion, when it really is well-founded. + This should be fixed by creating private functions to do the + recursion here, and leaving the (public-facing) + isWellFounded() call as the base of that recursion. Then we + can distinguish the cases. + */ + /* + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), false); + */ + return false; + } + } + + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), true); + return true; +} + +Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr(); + if(!groundTerm.isNull()) { + return groundTerm; + } + + RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + // Recursive path, we should skip and go to the next constructor; + // see lengthy comments in Datatype::mkGroundTerm(). + return Expr(); + } + + std::vector<Expr> groundTerms; + groundTerms.push_back(getConstructor()); + + // for each selector, get a ground term + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + groundTerms.push_back(SelectorType((*i).getSelector().getType()).getRangeType().mkGroundTerm()); + } + + groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + return groundTerm; +} + const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const { CheckArgument(index < getNumArgs(), index, "index out of bounds"); return d_args[index]; @@ -346,7 +637,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { // These datatype things are recursive! Be very careful not to // print an infinite chain of them. long& printNameOnly = os.iword(s_printDatatypeNamesOnly); - Debug("datatypes") << "printNameOnly is " << printNameOnly << std::endl; + Debug("datatypes-output") << "printNameOnly is " << printNameOnly << std::endl; if(printNameOnly) { return os << dt.getName(); } @@ -360,7 +651,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { } scope(printNameOnly, 1); // when scope is destructed, the value pops back - Debug("datatypes") << "printNameOnly is now " << printNameOnly << std::endl; + Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl; // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); diff --git a/src/util/datatype.h b/src/util/datatype.h index 74bff1843..df7dd1814 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -99,8 +99,17 @@ public: */ class CVC4_PUBLIC Datatype { public: - static const Datatype& datatypeOf(Expr item); - static size_t indexOf(Expr item); + /** + * Get the datatype of a constructor, selector, or tester operator. + */ + static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC; + + /** + * Get the index of a constructor or tester in its datatype, or the + * index of a selector in its constructor. (Zero is always the + * first index.) + */ + static size_t indexOf(Expr item) CVC4_PUBLIC; /** * A holder type (used in calls to Datatype::Constructor::addArg()) @@ -244,6 +253,33 @@ public: inline size_t getNumArgs() const throw(); /** + * Return the cardinality of this constructor (the product of the + * cardinalities of its arguments). + */ + Cardinality getCardinality() const throw(AssertionException); + + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite). This function can + * only be called for resolved constructors. + */ + bool isFinite() const throw(AssertionException); + + /** + * Return true iff this constructor is well-founded (there exist + * ground terms). The constructor must be resolved or an + * exception is thrown. + */ + bool isWellFounded() const throw(AssertionException); + + /** + * Construct and return a ground term of this constructor. The + * constructor must be both resolved and well-founded, or else an + * exception is thrown. + */ + Expr mkGroundTerm() const throw(AssertionException); + + /** * Returns true iff this Datatype constructor has already been * resolved. */ @@ -272,6 +308,7 @@ private: std::string d_name; std::vector<Constructor> d_constructors; bool d_resolved; + Type d_self; /** * Datatypes refer to themselves, recursively, and we have a @@ -303,6 +340,40 @@ public: inline size_t getNumConstructors() const throw(); /** + * Return the cardinality of this datatype (the sum of the + * cardinalities of its constructors). The Datatype must be + * resolved. + */ + Cardinality getCardinality() const throw(AssertionException); + + /** + * Return true iff this Datatype is finite (all constructors are + * finite, i.e., there are finitely many ground terms). If the + * datatype is not well-founded, this function returns false. The + * Datatype must be resolved or an exception is thrown. + */ + bool isFinite() const throw(AssertionException); + + /** + * Return true iff this datatype is well-founded (there exist ground + * terms). The Datatype must be resolved or an exception is thrown. + */ + bool isWellFounded() const throw(AssertionException); + + /** + * Construct and return a ground term of this Datatype. The + * Datatype must be both resolved and well-founded, or else an + * exception is thrown. + */ + Expr mkGroundTerm() const throw(AssertionException); + + /** + * Get the DatatypeType associated to this Datatype. Can only be + * called post-resolution. + */ + DatatypeType getDatatypeType() const throw(AssertionException); + + /** * Return true iff the two Datatypes are the same. * * We need == for mkConst(Datatype) to properly work---since if the @@ -372,7 +443,8 @@ inline std::string Datatype::UnresolvedType::getName() const throw() { inline Datatype::Datatype(std::string name) : d_name(name), d_constructors(), - d_resolved(false) { + d_resolved(false), + d_self() { } inline std::string Datatype::getName() const throw() { diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h new file mode 100644 index 000000000..6f82eec5c --- /dev/null +++ b/src/util/recursion_breaker.h @@ -0,0 +1,133 @@ +/********************* */ +/*! \file recursion_breaker.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A utility class to help with detecting recursion in a + ** computation + ** + ** A utility class to help with detecting recursion in a computation. + ** A breadcrumb trail is left, and a function can query the breaker + ** to see if recursion has occurred. For example: + ** + ** int foo(int x) { + ** RecursionBreaker<int> breaker("foo", x); + ** if(breaker.isRecursion()) { + ** ++d_count; + ** return 0; + ** } + ** int xfactor = x * x; + ** if(x > 0) { + ** xfactor = -xfactor; + ** } + ** int y = foo(11 * x + xfactor); + ** int z = y < 0 ? y : x * y; + ** cout << "x == " << x << ", y == " << y << " ==> " << z << endl; + ** return z; + ** } + ** + ** Recursion occurs after a while in this example, and the recursion + ** is broken by the RecursionBreaker. + ** + ** RecursionBreaker is really just a thread-local set of "what has + ** been seen." The above example is trivial, easily fixed by + ** allocating such a set at the base of the recursion, and passing a + ** reference to it to each invocation. But other cases of + ** nontrivial, mutual recursion exist that aren't so easily broken, + ** and that's what the RecursionBreaker is for. See + ** Datatype::getCardinality(), for example. A Datatype's cardinality + ** depends on the cardinalities of the types it references---but + ** these, in turn can reference the original datatype in a cyclic + ** fashion. Where that happens, we need to break the recursion. + ** + ** Several RecursionBreakers can be used at once; each is identified + ** by the string tag in its constructor. If a single function is + ** involved in the detection of recursion, a good choice is to use + ** __FUNCTION__: + ** + ** RecursionBreaker<Foo*>(__FUNCTION__, this) breaker; + ** + ** Of course, if you're using GNU, you might prefer + ** __PRETTY_FUNCTION__, since it's robust to overloading, namespaces, + ** and containing classes. But neither is a good choice if two + ** functions need to access the same RecursionBreaker mechanism. + ** + ** For non-primitive datatypes, it might be a good idea to use a + ** pointer type to instantiate RecursionBreaker<>, for example with + ** RecursionBreaker<Foo*>. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RECURSION_BREAKER_H +#define __CVC4__RECURSION_BREAKER_H + +#include <string> +#include <map> +#include <ext/hash_set> +#include "util/hash.h" +#include "util/tls.h" +#include "util/Assert.h" + +namespace CVC4 { + +template <class T> +class RecursionBreaker { + //typedef std::hash_set<T> Set; + typedef std::set<T> Set; + typedef std::map<std::string, Set> Map; + static CVC4_THREADLOCAL(Map*) s_maps; + + std::string d_tag; + const T& d_item; + bool d_firstToTag; + bool d_recursion; + +public: + RecursionBreaker(std::string tag, const T& item) : + d_tag(tag), + d_item(item) { + if(s_maps == NULL) { + s_maps = new Map(); + } + d_firstToTag = s_maps->find(tag) == s_maps->end(); + Set& set = (*s_maps)[tag]; + d_recursion = (set.find(item) != set.end()); + Assert(!d_recursion || !d_firstToTag); + if(!d_recursion) { + set.insert(item); + } + } + + ~RecursionBreaker() { + Assert(s_maps->find(d_tag) != s_maps->end()); + if(!d_recursion) { + (*s_maps)[d_tag].erase(d_item); + } + if(d_firstToTag) { + Assert((*s_maps)[d_tag].empty()); + s_maps->erase(d_tag); + Assert(s_maps->find(d_tag) == s_maps->end()); + } + } + + bool isRecursion() const throw() { + return d_recursion; + } + +};/* class RecursionBreaker<T> */ + +template <class T> +CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps; + +}/* CVC4 namespace */ + +#endif /* __CVC4__RECURSION_BREAKER_H */ |