summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_manager_template.cpp19
-rw-r--r--src/expr/expr_manager_template.h12
-rw-r--r--src/expr/node_manager.cpp28
-rw-r--r--src/expr/node_manager.h16
-rw-r--r--src/expr/type.cpp2
-rw-r--r--src/printer/cvc/cvc_printer.cpp30
-rw-r--r--src/printer/smt2/smt2_printer.cpp3
7 files changed, 64 insertions, 46 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 1981d0a7d..8bf8d9e54 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -115,10 +115,11 @@ ExprManager::~ExprManager()
}
}
#endif
+ // clear the datatypes
+ d_ownedDatatypes.clear();
delete d_nodeManager;
d_nodeManager = NULL;
-
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << std::endl
<< e << std::endl;
@@ -676,10 +677,11 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
std::map<std::string, DatatypeType> nameResolutions;
std::vector<DatatypeType> dtts;
- //have to build deep copy so that datatypes will live in NodeManager
+ // have to build deep copy so that datatypes will live in this class
std::vector< Datatype* > dt_copies;
for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
- dt_copies.push_back( new Datatype( *i ) );
+ d_ownedDatatypes.push_back(std::unique_ptr<Datatype>(new Datatype(*i)));
+ dt_copies.push_back(d_ownedDatatypes.back().get());
}
// First do some sanity checks, set up the final Type to be used for
@@ -689,12 +691,12 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
// pred selector.
for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) {
TypeNode* typeNode;
+ // register datatype with the node manager
+ unsigned index = d_nodeManager->registerDatatype((*i)->d_internal);
if( (*i)->getNumParameters() == 0 ) {
- unsigned index = d_nodeManager->registerDatatype( *i );
typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)));
//typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
} else {
- unsigned index = d_nodeManager->registerDatatype( *i );
TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index));
//TypeNode cons = d_nodeManager->mkTypeConst(*i);
std::vector< TypeNode > params;
@@ -1098,6 +1100,13 @@ Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapColle
new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
}
+const Datatype& ExprManager::getDatatypeForIndex(unsigned index) const
+{
+ // when the Node-level API is in place, this function will be deleted.
+ Assert(index < d_ownedDatatypes.size());
+ return *d_ownedDatatypes[index];
+}
+
${mkConst_implementations}
}/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 44871ff99..c61c7e012 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -79,9 +79,11 @@ private:
// undefined, private copy constructor and assignment op (disallow copy)
ExprManager(const ExprManager&) = delete;
ExprManager& operator=(const ExprManager&) = delete;
-
-public:
+ /** A list of datatypes owned by this expr manager. */
+ std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
+
+ public:
/**
* Creates an expression manager with default options.
*/
@@ -571,6 +573,12 @@ public:
/** Returns the maximum arity of the given kind. */
static unsigned maxArity(Kind kind);
+ /**
+ * Return the datatype at the given index owned by this class. Type nodes are
+ * associated with datatypes through the DatatypeIndexConstant class. The
+ * argument index is intended to be a value taken from that class.
+ */
+ const Datatype& getDatatypeForIndex(unsigned index) const;
};/* class ExprManager */
${mkConst_instantiations}
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0c3f1b4cb..39be675ec 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -187,15 +187,7 @@ NodeManager::~NodeManager() {
d_rt_cache.d_children.clear();
d_rt_cache.d_data = dummy;
- // TODO: switch to DType
- 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();
+ d_ownedDTypes.clear();
Assert(!d_attrManager->inGarbageCollection());
@@ -248,23 +240,17 @@ NodeManager::~NodeManager() {
d_options = NULL;
}
-unsigned NodeManager::registerDatatype(Datatype* dt) {
- unsigned sz = d_ownedDatatypes.size();
- d_ownedDatatypes.push_back( dt );
+size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt)
+{
+ size_t sz = d_ownedDTypes.size();
+ d_ownedDTypes.push_back(dt);
return sz;
}
-const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{
- // when the Node-level API is in place, this function will be deleted.
- Assert(index < d_ownedDatatypes.size());
- return *d_ownedDatatypes[index];
-}
-
const DType& NodeManager::getDTypeForIndex(unsigned index) const
{
- const Datatype& d = getDatatypeForIndex(index);
- // return its internal representation
- return *d.d_internal;
+ Assert(index < d_ownedDTypes.size());
+ return *d_ownedDTypes[index];
}
void NodeManager::reclaimZombies() {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 61ef1d39d..eced00c48 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -178,7 +178,7 @@ class NodeManager {
std::vector<NodeManagerListener*> d_listeners;
/** A list of datatypes owned by this node manager. */
- std::vector<Datatype*> d_ownedDatatypes;
+ std::vector<std::shared_ptr<DType> > d_ownedDTypes;
/**
* A map of tuple and record types to their corresponding datatype.
@@ -428,9 +428,17 @@ public:
}
/** register datatype */
- unsigned registerDatatype(Datatype* dt);
- /** get datatype for index */
- const Datatype & getDatatypeForIndex( unsigned index ) const;
+ size_t registerDatatype(std::shared_ptr<DType> dt);
+ /**
+ * Return the datatype at the given index owned by this class. Type nodes are
+ * associated with datatypes through the DatatypeIndexConstant class. The
+ * argument index is intended to be a value taken from that class.
+ *
+ * Type nodes must access their DTypes through a level of indirection to
+ * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
+ * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
+ * which is used as an index to retrieve the DType via this call.
+ */
const DType& getDTypeForIndex(unsigned index) const;
/** Get a Kind from an operator expression */
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 99fe73c22..031dcb3f0 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -576,7 +576,7 @@ const Datatype& DatatypeType::getDatatype() const {
if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
{
DatatypeIndexConstant dic = d_typeNode->getConst<DatatypeIndexConstant>();
- return d_nodeManager->getDatatypeForIndex(dic.getIndex());
+ return d_nodeManager->toExprManager()->getDatatypeForIndex(dic.getIndex());
}
Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE);
return DatatypeType((*d_typeNode)[0].toType()).getDatatype();
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 22a491af5..f8448f1e9 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -24,11 +24,12 @@
#include <typeinfo>
#include <vector>
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "printer/dagification_visitor.h"
+#include "expr/dtype.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
#include "options/smt_options.h"
+#include "printer/dagification_visitor.h"
#include "smt/command.h"
#include "smt/smt_engine.h"
#include "smt_util/node_visitor.h"
@@ -179,7 +180,9 @@ void CvcPrinter::toStream(
break;
case kind::DATATYPE_TYPE: {
- const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
+ const Datatype& dt =
+ NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
+ n.getConst<DatatypeIndexConstant>().getIndex());
if( dt.isTuple() ){
out << '[';
for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
@@ -347,14 +350,17 @@ void CvcPrinter::toStream(
// DATATYPES
case kind::PARAMETRIC_DATATYPE: {
- const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() ));
- out << dt.getName() << '[';
- for(unsigned i = 1; i < n.getNumChildren(); ++i) {
- if(i > 1) {
- out << ',';
- }
- out << n[i];
+ const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
+ n[0].getConst<DatatypeIndexConstant>().getIndex());
+ out << dt.getName() << '[';
+ for (unsigned i = 1; i < n.getNumChildren(); ++i)
+ {
+ if (i > 1)
+ {
+ out << ',';
}
+ out << n[i];
+ }
out << ']';
}
return;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 006895df7..f0a1e740f 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -21,6 +21,7 @@
#include <typeinfo>
#include <vector>
+#include "expr/dtype.h"
#include "expr/node_manager_attributes.h"
#include "options/bv_options.h"
#include "options/language.h"
@@ -246,7 +247,7 @@ void Smt2Printer::toStream(std::ostream& out,
case kind::DATATYPE_TYPE:
{
- const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex(
+ const DType& dt = (NodeManager::currentNM()->getDTypeForIndex(
n.getConst<DatatypeIndexConstant>().getIndex()));
if (dt.isTuple())
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback