Minor refactoring in preparation for datatypes node cycle breaking.

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 001f38a79499916f95006b0af072ec2d2cdfca57..a7039110f09420a4dd52eaf56a328a09fa5d2148 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -1105,4 +1105,9 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
   return os;
 }
 
+DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException) : d_index(index){
+
+}
+
+
 }/* CVC4 namespace */

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index dfd893fe8288b789923a7a4bd272e6e9435251b4..06735262d44fb472e0f096185e121ccb23130d5b 100644 (file)
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -757,6 +757,49 @@ struct CVC4_PUBLIC DatatypeHashFunction {
   }
 };/* struct DatatypeHashFunction */
 
+
+
+/* stores an index to Datatype residing in NodeManager */
+class CVC4_PUBLIC DatatypeIndexConstant {
+public:
+
+  DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException);
+
+  ~DatatypeIndexConstant() throw() { }
+
+  const unsigned getIndex() const throw() {
+    return d_index;
+  }
+  bool operator==(const DatatypeIndexConstant& uc) const throw() {
+    return d_index == uc.d_index;
+  }
+  bool operator!=(const DatatypeIndexConstant& uc) const throw() {
+    return !(*this == uc);
+  }
+  bool operator<(const DatatypeIndexConstant& uc) const throw() {
+    return d_index < uc.d_index;
+  }
+  bool operator<=(const DatatypeIndexConstant& uc) const throw() {
+    return d_index <= uc.d_index;
+  }
+  bool operator>(const DatatypeIndexConstant& uc) const throw() {
+    return !(*this <= uc);
+  }
+  bool operator>=(const DatatypeIndexConstant& uc) const throw() {
+    return !(*this < uc);
+  }
+private:
+  const unsigned d_index;
+};/* class DatatypeIndexConstant */
+
+struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
+  inline size_t operator()(const DatatypeIndexConstant& uc) const {
+    return IntegerHashFunction()(uc.getIndex());
+  }
+};/* struct DatatypeIndexConstantHashFunction */
+
+
+
 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
 
 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f7e76c06b2928a3e450018a7904c38006c7e00e2..af4f89da1bb6784c35b20a3a80a6ab4406d5e3e1 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -176,6 +176,13 @@ NodeManager::~NodeManager() {
   d_tt_cache.d_children.clear();
   d_rt_cache.d_children.clear();
 
+  for( std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(),      datatype_end = d_ownedDatatypes.end(); 
+       datatype_iter != datatype_end; ++datatype_iter) {
+    Datatype* datatype = *datatype_iter;
+    delete datatype;
+  }
+  d_ownedDatatypes.clear();
+
   Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
     reclaimZombies();

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3c3636d5fdcb691249084630db7610bff83e7ca1..aa78c9627ccd8f5825a332bec414ec6ac131db5e 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -165,6 +165,9 @@ class NodeManager {
    * A list of subscribers for NodeManager events.
    */
   std::vector<NodeManagerListener*> d_listeners;
+  
+  /** A list of datatypes owned by this node manager. */
+  std::vector<Datatype*> d_ownedDatatypes;
 
   /**
    * A map of tuple and record types to their corresponding datatype.

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 0c4d554ef9fb358ce5549098bda0539a356b74c7..18157016f880299c77700ba673001d883b988140 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -566,7 +566,7 @@ const Datatype& DatatypeType::getDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   if( d_typeNode->isParametricDatatype() ) {
     PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
-    const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
+    const Datatype& dt = (*d_typeNode)[0].getDatatype();
     return dt;
   } else {
     return d_typeNode->getDatatype();

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index dc2370bead5bf2b52a8f45516fb85415a7588bb0..ede710dad1a2c157dae383e388171b6561551971 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -275,14 +275,14 @@ bool TypeNode::isRecord() const {
 
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
-  const Datatype& dt = getConst<Datatype>();
+  const Datatype& dt = getDatatype();
   Assert(dt.getNumConstructors()==1);
   return dt[0].getNumArgs();
 }
 
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
-  const Datatype& dt = getConst<Datatype>();
+  const Datatype& dt = getDatatype();
   Assert(dt.getNumConstructors()==1);
   vector<TypeNode> types;
   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
@@ -315,7 +315,7 @@ bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() != kind::PARAMETRIC_DATATYPE) {
     return false;
   }
-  const Datatype& dt = (*this)[0].getConst<Datatype>();
+  const Datatype& dt = (*this)[0].getDatatype();
   unsigned n = dt.getNumParameters();
   Assert(n < getNumChildren());
   for(unsigned i = 0; i < n; ++i) {
@@ -329,7 +329,7 @@ bool TypeNode::isInstantiatedDatatype() const {
 /** Is this an instantiated datatype parameter */
 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
-  const Datatype& dt = (*this)[0].getConst<Datatype>();
+  const Datatype& dt = (*this)[0].getDatatype();
   AssertArgument(n < dt.getNumParameters(), *this);
   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 }

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 8957ad7f75d6e65fbd79a12e1f9f7bbd689a369a..51ae0fd11b35128b73c4223496481adadc109d95 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -332,7 +332,7 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext)
   if(type.getKind() == kind::DATATYPE_TYPE ||
      type.getKind() == kind::PARAMETRIC_DATATYPE) {
     bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE);
-    const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>();
+    const Datatype& dt = parametric ? type[0].getDatatype() : type.getDatatype();
     TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
     Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
     if(parametric) {
@@ -647,10 +647,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
                  t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
           const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
-            t[t.getNumChildren() - 1].getConst<Datatype>() :
-            t[t.getNumChildren() - 1][0].getConst<Datatype>();
+            t[t.getNumChildren() - 1].getDatatype() :
+            t[t.getNumChildren() - 1][0].getDatatype();
           TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
+          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype();
           if(dt != dt2) {
             Assert(d_varCache.find(top) != d_varCache.end(),
                    "constructor `%s' not in cache", top.toString().c_str());
@@ -665,10 +665,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         } else if(t.isTester() || t.isSelector()) {
           Assert(parentTheory != theory::THEORY_BOOL);
           const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
-            t[0].getConst<Datatype>() :
-            t[0][0].getConst<Datatype>();
+            t[0].getDatatype() :
+            t[0][0].getDatatype();
           TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
+          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype();
           if(dt != dt2) {
             Assert(d_varCache.find(top) != d_varCache.end(),
                    "tester or selector `%s' not in cache", top.toString().c_str());

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 369c5d48fa3aa97acd873019b2932e3681f2e63f..5988d81f9fee5cd63adf6e17ba26b0434587a489 100644 (file)
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -67,7 +67,7 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
       return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u));
     }
     if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) {
-      const Datatype& asDatatype = asType.getConst<Datatype>();
+      const Datatype& asDatatype = asType.getDatatype();
       return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
     }
   }

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 3338e5f3152a37b527994fbed2e2aaa393de279a..28a6a52d925bbff7961a5a118ec45f33cd24a9c4 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -44,11 +44,11 @@ constant DATATYPE_TYPE \
     "expr/datatype.h" \
     "a datatype type"
 cardinality DATATYPE_TYPE \
-    "%TYPE%.getConst<Datatype>().getCardinality()" \
+    "%TYPE%.getDatatype().getCardinality()" \
     "expr/datatype.h"
 well-founded DATATYPE_TYPE \
-    "%TYPE%.getConst<Datatype>().isWellFounded()" \
-    "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
+    "%TYPE%.getDatatype().isWellFounded()" \
+    "%TYPE%.getDatatype().mkGroundTerm(%TYPE%.toType())" \
     "expr/datatype.h"
 
 enumerator DATATYPE_TYPE \