summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am1
-rw-r--r--src/util/datatype.cpp303
-rw-r--r--src/util/datatype.h78
-rw-r--r--src/util/recursion_breaker.h133
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback