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

1 files changed, 6 insertions, 1 deletions

diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index c1da288a4..7a5bdbfb4 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -56,6 +56,11 @@ public:
           ? NodeManager::currentNM()
           : e.getExprManager()->getNodeManager()) {
   }
+  inline ExprManagerScope(const Type& t) :
+    d_nms(t.getExprManager() == NULL
+          ? NodeManager::currentNM()
+          : t.getExprManager()->getNodeManager()) {
+  }
   inline ExprManagerScope(const ExprManager& exprManager) :
     d_nms(exprManager.getNodeManager()) {
   }