summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/datatype.cpp5
-rw-r--r--src/expr/datatype.h43
-rw-r--r--src/expr/node_manager.cpp7
-rw-r--r--src/expr/node_manager.h3
-rw-r--r--src/expr/type.cpp2
-rw-r--r--src/expr/type_node.cpp8
-rw-r--r--src/smt/boolean_terms.cpp14
-rw-r--r--src/smt/model_postprocessor.cpp2
-rw-r--r--src/theory/datatypes/kinds6
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<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 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<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 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<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 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<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 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<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 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<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 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<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 \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback