From 3506b13f4d298095e8405b32b05e838f17dbe809 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 31 Oct 2016 10:45:27 -0500 Subject: [PATCH] Minor refactoring in preparation for datatypes node cycle breaking. --- src/expr/datatype.cpp | 5 ++++ src/expr/datatype.h | 43 +++++++++++++++++++++++++++++++++ src/expr/node_manager.cpp | 7 ++++++ src/expr/node_manager.h | 3 +++ src/expr/type.cpp | 2 +- src/expr/type_node.cpp | 8 +++--- src/smt/boolean_terms.cpp | 14 +++++------ src/smt/model_postprocessor.cpp | 2 +- src/theory/datatypes/kinds | 6 ++--- 9 files changed, 74 insertions(+), 16 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 001f38a79..a7039110f 100644 --- 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 dfd893fe8..06735262d 100644 --- 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 f7e76c06b..af4f89da1 100644 --- 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::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 3c3636d5f..aa78c9627 100644 --- 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 d_listeners; + + /** A list of datatypes owned by this node manager. */ + std::vector 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 0c4d554ef..18157016f 100644 --- 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(); + 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 dc2370bea..ede710dad 100644 --- 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(); + const Datatype& dt = getDatatype(); Assert(dt.getNumConstructors()==1); return dt[0].getNumArgs(); } vector TypeNode::getTupleTypes() const { Assert(isTuple()); - const Datatype& dt = getConst(); + const Datatype& dt = getDatatype(); Assert(dt.getNumConstructors()==1); vector 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(); + 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(); + 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 8957ad7f7..51ae0fd11 100644 --- 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() : type.getConst(); + 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() : - t[t.getNumChildren() - 1][0].getConst(); + 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(); + 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() : - t[0][0].getConst(); + 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(); + 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 369c5d48f..5988d81f9 100644 --- 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(); + 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 3338e5f31..28a6a52d9 100644 --- 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().getCardinality()" \ + "%TYPE%.getDatatype().getCardinality()" \ "expr/datatype.h" well-founded DATATYPE_TYPE \ - "%TYPE%.getConst().isWellFounded()" \ - "%TYPE%.getConst().mkGroundTerm(%TYPE%.toType())" \ + "%TYPE%.getDatatype().isWellFounded()" \ + "%TYPE%.getDatatype().mkGroundTerm(%TYPE%.toType())" \ "expr/datatype.h" enumerator DATATYPE_TYPE \ -- 2.30.2