summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/datatype.cpp4
-rw-r--r--src/expr/datatype.h9
-rw-r--r--src/expr/datatype.i14
-rw-r--r--src/expr/expr.i2
-rw-r--r--src/expr/expr_manager.i2
-rw-r--r--src/expr/expr_manager_template.cpp64
-rw-r--r--src/expr/expr_manager_template.h12
-rw-r--r--src/expr/node_manager.cpp28
-rw-r--r--src/expr/node_manager.h7
-rw-r--r--src/expr/type.cpp2
-rw-r--r--src/expr/type_node.h4
11 files changed, 100 insertions, 48 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index a7039110f..26ab2f2da 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -52,6 +52,7 @@ typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAtt
typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
Datatype::~Datatype(){
+ Trace("ajr-temp") << "delete datatype " << getName() << " " << this << std::endl;
delete d_record;
}
@@ -1109,5 +1110,8 @@ DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgume
}
+std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
+ return out << "index_" << dic.getIndex();
+}
}/* CVC4 namespace */
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 06735262d..f81d2358d 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -28,7 +28,8 @@
namespace CVC4 {
// messy; Expr needs Datatype (because it's the payload of a
// CONSTANT-kinded expression), and Datatype needs Expr.
- class CVC4_PUBLIC Datatype;
+ //class CVC4_PUBLIC Datatype;
+ class CVC4_PUBLIC DatatypeIndexConstant;
}/* CVC4 namespace */
#include "base/exception.h"
@@ -792,9 +793,11 @@ private:
const unsigned d_index;
};/* class DatatypeIndexConstant */
+std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) CVC4_PUBLIC;
+
struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
- inline size_t operator()(const DatatypeIndexConstant& uc) const {
- return IntegerHashFunction()(uc.getIndex());
+ inline size_t operator()(const DatatypeIndexConstant& dic) const {
+ return IntegerHashFunction()(dic.getIndex());
}
};/* struct DatatypeIndexConstantHashFunction */
diff --git a/src/expr/datatype.i b/src/expr/datatype.i
index a7456df38..a903e0241 100644
--- a/src/expr/datatype.i
+++ b/src/expr/datatype.i
@@ -75,6 +75,20 @@
%feature("valuewrapper") CVC4::DatatypeUnresolvedType;
%feature("valuewrapper") CVC4::DatatypeConstructor;
+
+%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const;
+%ignore CVC4::DatatypeIndexConstant::operator!=(const DatatypeIndexConstant&) const;
+
+%rename(less) CVC4::DatatypeIndexConstant::operator<(const DatatypeIndexConstant&) const;
+%rename(lessEqual) CVC4::DatatypeIndexConstant::operator<=(const DatatypeIndexConstant&) const;
+%rename(greater) CVC4::DatatypeIndexConstant::operator>(const DatatypeIndexConstant&) const;
+%rename(greaterEqual) CVC4::DatatypeIndexConstant::operator>=(const DatatypeIndexConstant&) const;
+
+%rename(apply) CVC4::DatatypeIndexConstantFunction::operator()(const DatatypeIndexConstant&) const;
+
+%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es);
+
+
#ifdef SWIGJAVA
// Instead of Datatype::begin() and end(), create an
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 354cacdc0..49cb24321 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -150,7 +150,7 @@ namespace CVC4 {
%template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>;
%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>;
%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>;
-%template(getConstDatatype) CVC4::Expr::getConst<CVC4::Datatype>;
+%template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>;
%template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>;
%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>;
%template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 11c1e284d..f8bb55523 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -65,7 +65,7 @@
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6d8497a60..525f8ead3 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -645,46 +645,52 @@ SetType ExprManager::mkSetType(Type elementType) const {
return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
}
-DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+DatatypeType ExprManager::mkDatatypeType(Datatype*& datatype) {
// Not worth a special implementation; this doesn't need to be fast
// code anyway.
- vector<Datatype> datatypes;
+ vector<Datatype*> datatypes;
datatypes.push_back(datatype);
- vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
+ std::vector<DatatypeType> result;
+ mkMutualDatatypeTypes(datatypes, result);
Assert(result.size() == 1);
return result.front();
}
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
- return mkMutualDatatypeTypes(datatypes, set<Type>());
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) {
+ std::set<Type> unresolvedTypes;
+ return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts);
}
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
- const std::set<Type>& unresolvedTypes) {
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) {
NodeManagerScope nms(d_nodeManager);
std::map<std::string, DatatypeType> nameResolutions;
- std::vector<DatatypeType> dtts;
+ Trace("ajr-temp") << "Build datatypes..." << std::endl;
+ //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 ) );
+ //}
+
+
// First do some sanity checks, set up the final Type to be used for
// each datatype, and set up the "named resolutions" used to handle
// simple self- and mutual-recursion, for example in the definition
// "nat = succ(pred:nat) | zero", a named resolution can handle the
// pred selector.
- for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
- i_end = datatypes.end();
- i != i_end;
- ++i) {
+ for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
TypeNode* typeNode;
- if( (*i).getNumParameters() == 0 ) {
- typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+ 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 {
- TypeNode cons = d_nodeManager->mkTypeConst(*i);
+ unsigned index = d_nodeManager->registerDatatype( *i );
+ TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index));
+ //TypeNode cons = d_nodeManager->mkTypeConst(*i);
std::vector< TypeNode > params;
params.push_back( cons );
- for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
- params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
+ for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) {
+ params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) );
}
typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
@@ -692,15 +698,19 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
Type type(d_nodeManager, typeNode);
DatatypeType dtt(type);
PrettyCheckArgument(
- nameResolutions.find((*i).getName()) == nameResolutions.end(),
+ nameResolutions.find((*i)->getName()) == nameResolutions.end(),
datatypes,
"cannot construct two datatypes at the same time "
"with the same name `%s'",
- (*i).getName().c_str());
- nameResolutions.insert(std::make_pair((*i).getName(), dtt));
+ (*i)->getName().c_str());
+ nameResolutions.insert(std::make_pair((*i)->getName(), dtt));
dtts.push_back(dtt);
+ //d_keep_dtt.push_back(dtt);
+ //d_keep_dt.push_back(*i);
+ //Assert( dtt.getDatatype()==(*i) );
}
+ Trace("ajr-temp") << "Set up map..." << std::endl;
// Second, set up the type substitution map for complex type
// resolution (e.g. if "list" is the type we're defining, and it has
// a selector of type "ARRAY INT OF list", this can't be taken care
@@ -714,10 +724,7 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
std::vector< DatatypeType > paramReplacements;
std::vector<Type> placeholders;// to hold the "unresolved placeholders"
std::vector<Type> replacements;// to hold our final, resolved types
- for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
- i_end = unresolvedTypes.end();
- i != i_end;
- ++i) {
+ for(std::set<Type>::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) {
std::string name;
if( (*i).isSort() ) {
name = SortType(*i).getName();
@@ -746,12 +753,14 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
}
}
+ Trace("ajr-temp") << "Resolve..." << std::endl;
// Lastly, perform the final resolutions and checks.
for(std::vector<DatatypeType>::iterator i = dtts.begin(),
i_end = dtts.end();
i != i_end;
++i) {
const Datatype& dt = (*i).getDatatype();
+ Trace("ajr-temp") << "Resolve " << dt.getName() << std::endl;
if(!dt.isResolved()) {
const_cast<Datatype&>(dt).resolve(this, nameResolutions,
placeholders, replacements,
@@ -763,11 +772,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
checkResolvedDatatype(*i);
}
+ Trace("ajr-temp") << "Notify..." << std::endl;
for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
(*i)->nmNotifyNewDatatypes(dtts);
}
- return dtts;
+ Trace("ajr-temp") << "Finish..." << std::endl;
}
void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 95b9c60bf..3f29396a3 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -87,6 +87,9 @@ private:
ExprManager(const ExprManager&) CVC4_UNDEFINED;
ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
+ std::vector<DatatypeType> d_keep_dtt;
+ std::vector<Datatype> d_keep_dt;
+
public:
/**
@@ -371,14 +374,13 @@ public:
SetType mkSetType(Type elementType) const;
/** Make a type representing the given datatype. */
- DatatypeType mkDatatypeType(const Datatype& datatype);
+ DatatypeType mkDatatypeType(Datatype*& datatype);
/**
* Make a set of types representing the given datatypes, which may be
* mutually recursive.
*/
- std::vector<DatatypeType>
- mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+ void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts);
/**
* Make a set of types representing the given datatypes, which may
@@ -409,9 +411,7 @@ public:
* then no complicated Type needs to be created, and the above,
* simpler form of mkMutualDatatypeTypes() is enough.
*/
- std::vector<DatatypeType>
- mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
- const std::set<Type>& unresolvedTypes);
+ void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts);
/**
* Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index af4f89da1..af0b1a2d0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -172,9 +172,11 @@ NodeManager::~NodeManager() {
d_unique_vars.clear();
- //d_tupleAndRecordTypes.clear();
+ TypeNode dummy;
d_tt_cache.d_children.clear();
+ d_tt_cache.d_data = dummy;
d_rt_cache.d_children.clear();
+ d_rt_cache.d_data = dummy;
for( std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(), datatype_end = d_ownedDatatypes.end();
datatype_iter != datatype_end; ++datatype_iter) {
@@ -217,6 +219,18 @@ NodeManager::~NodeManager() {
d_options = NULL;
}
+unsigned NodeManager::registerDatatype(Datatype* dt) {
+ Trace("ajr-temp") << "Register datatype : " << dt->getName() << " " << dt << std::endl;
+ unsigned sz = d_ownedDatatypes.size();
+ d_ownedDatatypes.push_back( dt );
+ return sz;
+}
+
+const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{
+ Assert( index<d_ownedDatatypes.size() );
+ return *d_ownedDatatypes[index];
+}
+
void NodeManager::reclaimZombies() {
// FIXME multithreading
Assert(!d_attrManager->inGarbageCollection());
@@ -475,15 +489,15 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
if( index==types.size() ){
if( d_data.isNull() ){
- Datatype dt("__cvc4_tuple");
- dt.setTuple();
+ Datatype* dt = new Datatype("__cvc4_tuple");
+ dt->setTuple();
DatatypeConstructor c("__cvc4_tuple_ctor");
for (unsigned i = 0; i < types.size(); ++ i) {
std::stringstream ss;
ss << "__cvc4_tuple_stor_" << i;
c.addArg(ss.str().c_str(), types[i].toType());
}
- dt.addConstructor(c);
+ dt->addConstructor(c);
d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
}
@@ -497,13 +511,13 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
if( index==rec.getNumFields() ){
if( d_data.isNull() ){
const Record::FieldVector& fields = rec.getFields();
- Datatype dt("__cvc4_record");
- dt.setRecord();
+ Datatype* dt = new Datatype("__cvc4_record");
+ dt->setRecord();
DatatypeConstructor c("__cvc4_record_ctor");
for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
c.addArg((*i).first, (*i).second);
}
- dt.addConstructor(c);
+ dt->addConstructor(c);
d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
}
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index aa78c9627..9342a02c4 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -84,7 +84,7 @@ class NodeManager {
friend Expr ExprManager::mkVar(Type, uint32_t flags);
// friend so it can access NodeManager's d_listeners and notify clients
- friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
+ friend void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>&, std::set<Type>&, std::vector<DatatypeType>&);
/** Predicate for use with STL algorithms */
struct NodeValueReferenceCountNonZero {
@@ -380,6 +380,11 @@ public:
Assert(elt != d_listeners.end(), "listener not subscribed");
d_listeners.erase(elt);
}
+
+ /** register datatype */
+ unsigned registerDatatype(Datatype* dt);
+ /** get datatype for index */
+ const Datatype & getDatatypeForIndex( unsigned index ) const;
/** Get a Kind from an operator expression */
static inline Kind operatorToKind(TNode n);
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 18157016f..11a45db79 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -608,7 +608,7 @@ std::vector<Type> DatatypeType::getParamTypes() const {
DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
NodeManagerScope nms(d_nodeManager);
- TypeNode cons = d_nodeManager->mkTypeConst( getDatatype() );
+ TypeNode cons = d_nodeManager->mkTypeConst( (*d_typeNode)[0].getConst<DatatypeIndexConstant>() );
vector<TypeNode> paramsNodes;
paramsNodes.push_back( cons );
for(vector<Type>::const_iterator i = params.begin(),
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0cada0df2..9fffbdeb2 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1023,7 +1023,9 @@ inline bool TypeNode::isBitVector(unsigned size) const {
/** Get the datatype specification from a datatype type */
inline const Datatype& TypeNode::getDatatype() const {
Assert(isDatatype());
- return getConst<Datatype>();
+ //return getConst<Datatype>();
+ DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
+ return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
}
/** Get the exponent size of this floating-point type */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback