diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/expr/node_manager.cpp | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 110 |
1 files changed, 52 insertions, 58 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e6e44928d..0809a0331 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): ACSYS, Kshitij Bansal, Tim King, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Expression manager implementation. ** @@ -170,7 +170,9 @@ NodeManager::~NodeManager() { d_operators[i] = Node::null(); } - d_tupleAndRecordTypes.clear(); + //d_tupleAndRecordTypes.clear(); + d_tt_cache.d_children.clear(); + d_rt_cache.d_children.clear(); Assert(!d_attrManager->inGarbageCollection() ); while(!d_zombies.empty()) { @@ -461,6 +463,47 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) return TypeNode(mkTypeConst(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(); + 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); + d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); + Debug("tuprec-debug") << "Return type : " << d_data << std::endl; + } + return d_data; + }else{ + return d_children[types[index]].getTupleType( nm, types, index+1 ); + } +} + +TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) { + if( index==rec.getNumFields() ){ + if( d_data.isNull() ){ + const Record::FieldVector& fields = rec.getFields(); + Datatype dt("__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); + d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); + Debug("tuprec-debug") << "Return type : " << d_data << std::endl; + } + return d_data; + }else{ + return d_children[TypeNode::fromType( rec[index].second )][rec[index].first].getRecordType( nm, rec, index+1 ); + } +} + TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { std::vector< TypeNode > ts; Debug("tuprec-debug") << "Make tuple type : "; @@ -470,60 +513,11 @@ TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { Debug("tuprec-debug") << types[i] << " "; } Debug("tuprec-debug") << std::endl; - //index based on function type - TypeNode tindex; - if( types.empty() ){ - //do nothing (will index on null type) - }else if( types.size()==1 ){ - tindex = types[0]; - }else{ - TypeNode tt = ts.back(); - ts.pop_back(); - tindex = mkFunctionType( ts, tt ); - ts.push_back( tt ); - } - TypeNode& dtt = d_tupleAndRecordTypes[tindex]; - if(dtt.isNull()) { - Datatype dt("__cvc4_tuple"); - dt.setTuple(); - DatatypeConstructor c("__cvc4_tuple_ctor"); - for (unsigned i = 0; i < ts.size(); ++ i) { - std::stringstream ss; - ss << "__cvc4_tuple_stor_" << i; - c.addArg(ss.str().c_str(), ts[i].toType()); - } - dt.addConstructor(c); - dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); - dtt.setAttribute(DatatypeTupleAttr(), tindex); - Debug("tuprec-debug") << "Return type : " << dtt << std::endl; - }else{ - Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; - } - Assert(!dtt.isNull()); - return dtt; + return d_tt_cache.getTupleType( this, ts ); } TypeNode NodeManager::mkRecordType(const Record& rec) { - //index based on type constant - TypeNode tindex = mkTypeConst(rec); - TypeNode& dtt = d_tupleAndRecordTypes[tindex]; - if(dtt.isNull()) { - const Record::FieldVector& fields = rec.getFields(); - Datatype dt("__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); - dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); - dtt.setAttribute(DatatypeRecordAttr(), tindex); - Debug("tuprec-debug") << "Return type : " << dtt << std::endl; - }else{ - Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; - } - Assert(!dtt.isNull()); - return dtt; + return d_rt_cache.getRecordType( this, rec ); } void NodeManager::reclaimAllZombies(){ |