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 | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/expr')
59 files changed, 633 insertions, 565 deletions
diff --git a/src/expr/array.h b/src/expr/array.h index ab554171f..cf050e077 100644 --- a/src/expr/array.h +++ b/src/expr/array.h @@ -1,13 +1,13 @@ /********************* */ /*! \file array.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Array types. ** diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 6ac07c81d..c8e346e48 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file array_store_all.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** 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 Representation of a constant array (an array in which the ** element is the same for all indices) diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 293b785a9..0a9c8344a 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -1,13 +1,13 @@ /********************* */ /*! \file array_store_all.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Representation of a constant array (an array in which the ** element is the same for all indices) diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index 42906e557..46d2871ff 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -1,13 +1,13 @@ /********************* */ /*! \file ascription_type.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 A class representing a type ascription ** diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index cd5b35384..3cf242988 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file attribute.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic, Tim King - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Dejan Jovanovic ** 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 AttributeManager implementation. ** diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 432fbbac9..13bedeaf8 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -1,13 +1,13 @@ /********************* */ /*! \file attribute.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** 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 Node attributes. ** diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index dae11fd74..60d2069e7 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -1,13 +1,13 @@ /********************* */ /*! \file attribute_internals.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** 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 Node attributes' internals. ** diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index 45dc368a5..4875bdf50 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -1,13 +1,13 @@ /********************* */ /*! \file attribute_unique_id.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** 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 [[ Add one-line brief description here ]] ** diff --git a/src/expr/chain.h b/src/expr/chain.h index e052a2ed8..703aa76ed 100644 --- a/src/expr/chain.h +++ b/src/expr/chain.h @@ -1,13 +1,13 @@ /********************* */ /*! \file chain.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 [[ Add one-line brief description here ]] ** diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h index 0c3b690b2..611a88e6f 100644 --- a/src/expr/convenience_node_builders.h +++ b/src/expr/convenience_node_builders.h @@ -1,13 +1,13 @@ /********************* */ /*! \file convenience_node_builders.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Convenience node builders. ** diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 32c0bb6dd..d14ac26d4 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file datatype.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** 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 A class representing a Datatype definition ** @@ -51,6 +51,10 @@ typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFin typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr; typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr; +Datatype::~Datatype(){ + delete d_record; +} + const Datatype& Datatype::datatypeOf(Expr item) { ExprManagerScope ems(item); TypeNode t = Node::fromExpr(item).getType(); @@ -133,6 +137,14 @@ void Datatype::resolve(ExprManager* em, d_involvesUt = true; } } + + if( d_isRecord ){ + std::vector< std::pair<std::string, Type> > fields; + for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){ + fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) ); + } + d_record = new Record(fields); + } } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -152,10 +164,12 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ } void Datatype::setTuple() { + PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype"); d_isTuple = true; } void Datatype::setRecord() { + PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype"); d_isRecord = true; } @@ -185,20 +199,24 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( d_card_rec_singleton==0 ){ - Assert( d_card_u_assume.empty() ); - std::vector< Type > processing; - if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){ - d_card_rec_singleton = 1; + if( isCodatatype() ){ + Assert( d_card_u_assume.empty() ); + std::vector< Type > processing; + if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){ + d_card_rec_singleton = 1; + }else{ + d_card_rec_singleton = -1; + } + if( d_card_rec_singleton==1 ){ + Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl; + for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ + Trace("dt-card") << " " << d_card_u_assume [i] << std::endl; + } + Trace("dt-card") << std::endl; + } }else{ d_card_rec_singleton = -1; } - if( d_card_rec_singleton==1 ){ - Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl; - for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ - Trace("dt-card") << " " << d_card_u_assume [i] << std::endl; - } - Trace("dt-card") << std::endl; - } } return d_card_rec_singleton==1; } @@ -288,10 +306,11 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + //start by assuming it is not + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), false); for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { if(! (*i).isUFinite()) { - self.setAttribute(DatatypeUFiniteComputedAttr(), true); - self.setAttribute(DatatypeUFiniteAttr(), false); return false; } } @@ -820,7 +839,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return self.getAttribute(DatatypeFiniteAttr()); } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { + if(! (*i).getRangeType().getCardinality().isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), false); return false; @@ -840,9 +859,18 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + bool success = true; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - Type t = SelectorType((*i).getSelector().getType()).getRangeType(); - if(!t.isSort() && !t.getCardinality().isFinite()) { + Type t = (*i).getRangeType(); + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)t).getDatatype(); + if( !dt.isUFinite() ){ + success = false; + } + }else if(!t.isSort() && !t.getCardinality().isFinite()) { + success = false; + } + if(!success ){ self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); return false; @@ -974,6 +1002,10 @@ SelectorType DatatypeConstructorArg::getType() const { return getSelector().getType(); } +Type DatatypeConstructorArg::getRangeType() const { + return getType().getRangeType(); +} + bool DatatypeConstructorArg::isUnresolvedSelf() const throw() { return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 625fbb5d4..1197b4a3b 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -1,13 +1,13 @@ /********************* */ /*! \file datatype.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** 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 A class representing a Datatype definition ** @@ -155,6 +155,11 @@ public: SelectorType getType() const; /** + * Get the range type of this argument. + */ + Type getRangeType() const; + + /** * Get the name of the type of this constructor argument * (Datatype field). Can be used for not-yet-resolved Datatypes * (in which case the name of the unresolved type, or "[self]" @@ -474,6 +479,7 @@ private: bool d_isCo; bool d_isTuple; bool d_isRecord; + Record * d_record; std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; @@ -553,6 +559,8 @@ public: */ inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false); + ~Datatype(); + /** * Add a constructor to this Datatype. Constructor names need not * be unique; they are for convenience and pretty-printing only. @@ -602,6 +610,9 @@ public: /** is this a record datatype? */ inline bool isRecord() const; + /** get the record representation for this datatype */ + inline Record * getRecord() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -772,6 +783,7 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_isCo(isCo), d_isTuple(false), d_isRecord(false), + d_record(NULL), d_constructors(), d_resolved(false), d_self(), @@ -788,6 +800,7 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo d_isCo(isCo), d_isTuple(false), d_isRecord(false), + d_record(NULL), d_constructors(), d_resolved(false), d_self(), @@ -844,6 +857,10 @@ inline bool Datatype::isRecord() const { return d_isRecord; } +inline Record * Datatype::getRecord() const { + return d_record; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index a6e2c1ece..23e6df7dc 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file emptyset.cpp ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Kshitij Bansal, Morgan Deters ** 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 [[ Add one-line brief description here ]] ** diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index cf9d050f8..a606951f0 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -1,13 +1,13 @@ /********************* */ /*! \file emptyset.h ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Kshitij Bansal, Morgan Deters ** 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 [[ Add one-line brief description here ]] ** diff --git a/src/expr/expr.i b/src/expr/expr.i index b50686f52..354cacdc0 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -130,7 +130,13 @@ namespace CVC4 { %include "expr/expr.h" +#ifdef SWIGPYTHON +/* The python bindings on Mac OS X have trouble with this one - leave it + * out for now. */ +//%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; +#else %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; +#endif %template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>; %template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>; %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>; diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp index 4c7ab3c8b..1d6df2a4e 100644 --- a/src/expr/expr_iomanip.cpp +++ b/src/expr/expr_iomanip.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_iomanip.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2015 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 Expr IO manipulation classes. ** diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index b3370e75a..94e2b46ea 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_iomanip.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2015 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 Expr IO manipulation classes. ** diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 66930cf55..11c1e284d 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -40,7 +40,6 @@ %include "expr/expr_manager.h" -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>; @@ -67,10 +66,7 @@ %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::TupleSelect>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>; @@ -78,6 +74,25 @@ %template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RegExp>; +#ifdef SWIGPYTHON +/* The python bindings cannot differentiate between bool and other basic + * types like enum and int. Therefore, we rename mkConst for the bool + * case into mkBoolConst. +*/ +%template(mkBoolConst) CVC4::ExprManager::mkConst<bool>; + +// These cases have trouble too. Remove them for now. +//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; +//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>; +//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>; +//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>; + +#else +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>; %template(mkConst) CVC4::ExprManager::mkConst<bool>; +#endif %include "expr/expr_manager.h" diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index a8e8f04be..cd4c274e5 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_manager_scope.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Tim King ** 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 [[ Add one-line brief description here ]] ** diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index ce7a92b48..84f674d2b 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_manager_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic, Christopher L. Conway - ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Christopher L. Conway ** 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 Public-facing expression manager interface, implementation ** @@ -142,6 +142,11 @@ StringType ExprManager::stringType() const { return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType()))); } +RegExpType ExprManager::regExpType() const { + NodeManagerScope nms(d_nodeManager); + return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType()))); +} + RealType ExprManager::realType() const { NodeManagerScope nms(d_nodeManager); return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType()))); @@ -791,7 +796,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { j != j_end; ++j) { const DatatypeConstructorArg& a = *j; - Type selectorType = a.getSelector().getType(); + Type selectorType = a.getType(); Assert(a.isResolved() && selectorType.isSelector() && SelectorType(selectorType).getDomain() == dtt, diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 37ef128f4..04f2f4289 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_manager_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic - ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** 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 Public-facing expression manager interface ** @@ -121,6 +121,9 @@ public: /** Get the type for strings. */ StringType stringType() const; + /** Get the type for regular expressions. */ + RegExpType regExpType() const; + /** Get the type for reals. */ RealType realType() const; diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h index 20977011c..d3dbd2902 100644 --- a/src/expr/expr_stream.h +++ b/src/expr/expr_stream.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_stream.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 A stream interface for expressions ** diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index a6cdedd00..43e4a7b76 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic, Kshitij Bansal - ** Minor contributors (to current version): Tim King, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Kshitij Bansal, Dejan Jovanovic ** 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 Public-facing expression interface, implementation. ** diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index d037a6bb9..5c3f89e9c 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic - ** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** 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 Public-facing expression interface. ** diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index 02e9728f0..6858f8ab9 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -1,13 +1,13 @@ /********************* */ /*! \file kind_map.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Dejan Jovanovic, Tim King ** 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 A bitmap of Kinds ** diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 799d1ac33..440d6b586 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file kind_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** 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 Template for the Node kind header ** diff --git a/src/expr/matcher.h b/src/expr/matcher.h index 8cb092a64..308ad06df 100644 --- a/src/expr/matcher.h +++ b/src/expr/matcher.h @@ -1,13 +1,13 @@ /********************* */ /*! \file matcher.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** 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 A class representing a type matcher ** diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 539db1c91..9025aa02a 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file metakind_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Template for the metakind header. ** diff --git a/src/expr/node.cpp b/src/expr/node.cpp index cf9a772b7..793b6af97 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file node.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** 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 Reference-counted encapsulation of a pointer to node information. ** diff --git a/src/expr/node.h b/src/expr/node.h index a51de6d66..998294da3 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot, Clark Barrett, Tim King, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** 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 Reference-counted encapsulation of a pointer to node information ** diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index e1a083a78..0dd4e44e8 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_builder.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Tim King, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** 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 A builder interface for Nodes. ** 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(){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 45c9afbde..7d2b13e4c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Christopher L. Conway, Morgan Deters - ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King + ** Top contributors (to current version): + ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ** 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 A manager for Nodes ** @@ -166,7 +166,20 @@ class NodeManager { /** * A map of tuple and record types to their corresponding datatype. */ - std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes; + class TupleTypeCache { + public: + std::map< TypeNode, TupleTypeCache > d_children; + TypeNode d_data; + TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 ); + }; + class RecTypeCache { + public: + std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children; + TypeNode d_data; + TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 ); + }; + TupleTypeCache d_tt_cache; + RecTypeCache d_rt_cache; /** * Keep a count of all abstract values produced by this NodeManager. @@ -692,7 +705,7 @@ public: inline TypeNode stringType(); /** Get the (singleton) type for RegExp. */ - inline TypeNode regexpType(); + inline TypeNode regExpType(); /** Get the (singleton) type for rounding modes. */ inline TypeNode roundingModeType(); @@ -988,7 +1001,7 @@ inline TypeNode NodeManager::stringType() { } /** Get the (singleton) type for regexps. */ -inline TypeNode NodeManager::regexpType() { +inline TypeNode NodeManager::regExpType() { return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE)); } diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index 41086ac21..20e1c6c50 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager_attributes.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 [[ Add one-line brief description here ]] ** @@ -28,8 +28,6 @@ namespace attr { struct VarNameTag { }; struct GlobalVarTag { }; struct SortArityTag { }; - struct DatatypeTupleTag { }; - struct DatatypeRecordTag { }; struct TypeTag { }; struct TypeCheckedTag { }; }/* CVC4::expr::attr namespace */ @@ -37,10 +35,6 @@ namespace attr { typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr; typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; -/** Attribute true for datatype types that are replacements for tuple types */ -typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr; -/** Attribute true for datatype types that are replacements for record types */ -typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr; typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr; typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr; diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp index ec2de105a..3915aa9bd 100644 --- a/src/expr/node_manager_listeners.cpp +++ b/src/expr/node_manager_listeners.cpp @@ -1,13 +1,13 @@ /********************* */ -/*! \file node_manager_listeners.h +/*! \file node_manager_listeners.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** 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 Listeners that NodeManager registers to its Options object. ** diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h index fc7c2f65f..caff3a545 100644 --- a/src/expr/node_manager_listeners.h +++ b/src/expr/node_manager_listeners.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager_listeners.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** 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 Listeners that NodeManager registers to its Options object. ** diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 77fc05e3b..9d37f6e6e 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_self_iterator.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Iterator supporting Node "self-iteration" ** diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index ab18973cb..a40075ca9 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file node_value.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Clark Barrett ** 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 An expression node. ** diff --git a/src/expr/node_value.h b/src/expr/node_value.h index c39c14604..fbf3ff76e 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_value.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Christopher L. Conway, Tim King, Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** 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 An expression node. ** diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp index e273bcece..2050d2d15 100644 --- a/src/expr/pickle_data.cpp +++ b/src/expr/pickle_data.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file pickle_data.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 This is a "pickle" for expressions, CVC4-internal view ** diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h index acf0dccdd..6c283719a 100644 --- a/src/expr/pickle_data.h +++ b/src/expr/pickle_data.h @@ -1,13 +1,13 @@ /********************* */ /*! \file pickle_data.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 This is a "pickle" for expressions, CVC4-internal view ** diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index d0501ca2b..ab8037a9a 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file pickler.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King, Kshitij Bansal + ** Top contributors (to current version): + ** Morgan Deters, Kshitij Bansal, Tim King ** 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 This is a "pickler" for expressions ** diff --git a/src/expr/pickler.h b/src/expr/pickler.h index cf1754d93..abd927788 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -1,13 +1,13 @@ /********************* */ /*! \file pickler.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Kshitij Bansal ** 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 This is a "pickler" for expressions ** diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp index 5ccc3484a..52b580148 100644 --- a/src/expr/predicate.cpp +++ b/src/expr/predicate.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file predicate.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** 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 Representation of predicates for predicate subtyping ** diff --git a/src/expr/predicate.h b/src/expr/predicate.h index 669ecc29f..a7003fbd1 100644 --- a/src/expr/predicate.h +++ b/src/expr/predicate.h @@ -1,13 +1,13 @@ /********************* */ /*! \file predicate.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Representation of predicates for predicate subtyping ** diff --git a/src/expr/record.cpp b/src/expr/record.cpp index ec5ef96f1..0d2fd6527 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file record.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** 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 A class representing a record definition ** diff --git a/src/expr/record.h b/src/expr/record.h index d30536fb0..84feb7e1d 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -1,13 +1,13 @@ /********************* */ /*! \file record.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 A class representing a Record definition ** diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index c0a80b7ce..185006e73 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file symbol_table.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Christopher L. Conway - ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot + ** Top contributors (to current version): + ** Morgan Deters, Christopher L. Conway, Tim King ** 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 Convenience class for scoping variable and type ** declarations (implementation) diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 451a482dc..efd0f1a13 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -1,13 +1,13 @@ /********************* */ /*! \file symbol_table.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Christopher L. Conway - ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot + ** Top contributors (to current version): + ** Morgan Deters, Christopher L. Conway, Francois Bobot ** 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 Convenience class for scoping variable and type declarations. ** diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 6b5bdf07c..0c4d554ef 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file type.cpp ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Dejan Jovanovic, Morgan Deters - ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, 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 Implementation of expression types ** @@ -223,6 +223,12 @@ bool Type::isString() const { return d_typeNode->isString(); } +/** Is this the regexp type? */ +bool Type::isRegExp() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isRegExp(); +} + /** Is this the rounding mode type? */ bool Type::isRoundingMode() const { NodeManagerScope nms(d_nodeManager); @@ -427,6 +433,11 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) : PrettyCheckArgument(isNull() || isString(), this); } +RegExpType::RegExpType(const Type& t) throw(IllegalArgumentException) : + Type(t) { + PrettyCheckArgument(isNull() || isRegExp(), this); +} + RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) : Type(t) { PrettyCheckArgument(isNull() || isRoundingMode(), this); diff --git a/src/expr/type.h b/src/expr/type.h index 67d259fec..43cb3ffbf 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Dejan Jovanovic, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Martin Brain ** 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 Interface for expression types. ** @@ -47,6 +47,7 @@ class BooleanType; class IntegerType; class RealType; class StringType; +class RegExpType; class RoundingModeType; class BitVectorType; class ArrayType; @@ -258,6 +259,12 @@ public: bool isString() const; /** + * Is this the regexp type? + * @return true if the type is the regexp type + */ + bool isRegExp() const; + + /** * Is this the rounding mode type? * @return true if the type is the rounding mode type */ @@ -424,6 +431,18 @@ public: };/* class StringType */ /** + * Singleton class encapsulating the string type. + */ +class CVC4_PUBLIC RegExpType : public Type { + +public: + + /** Construct from the base type */ + RegExpType(const Type& type) throw(IllegalArgumentException); +};/* class RegExpType */ + + +/** * Singleton class encapsulating the rounding mode type. */ class CVC4_PUBLIC RoundingModeType : public Type { diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index 4b04adfc9..3df73b268 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type_checker.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 A type checker ** diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 061e1b4e0..8ed894a22 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file type_checker_template.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 TypeChecker implementation ** diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 755b16e46..5d672e6ac 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file type_node.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Kshitij Bansal, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tim King + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Kshitij Bansal ** 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 Reference-counted encapsulation of a pointer to node information. ** @@ -93,46 +93,28 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { t.getConst<TypeConstant>() == REAL_TYPE ); } } - if(isTuple() || isRecord()) { - if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { + if(isTuple() && t.isTuple()) { + const Datatype& dt1 = getDatatype(); + const Datatype& dt2 = t.getDatatype(); + if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){ return false; } - if(isTuple()) { - if(getNumChildren() != t.getNumChildren()) { + // r1's fields must be subtypes of r2's, in order + for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){ + if( !dt1[0][i].getRangeType().isSubtypeOf( dt2[0][i].getRangeType() ) ){ return false; } - // children must be subtypes of t's, in order - for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { - if(!(*i).isSubtypeOf(*j)) { - return false; - } - } - } else { - const Record& r1 = getRecord(); - const Record& r2 = t.getRecord(); - if(r1.getNumFields() != r2.getNumFields()) { - return false; - } - const Record::FieldVector& fields1 = r1.getFields(); - const Record::FieldVector& fields2 = r2.getFields(); - // r1's fields must be subtypes of r2's, in order - // names must match also - for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) { - if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) { - return false; - } - } } return true; + }else if( t.isRecord() && t.isRecord() ){ + //records are not subtypes of each other in current implementation } if(isFunction()) { // A function is a subtype of another if the args are the same type, and // the return type is a subtype of the other's. This is enough for now // (and it's necessary for model generation, since a Real-valued function // might return a constant Int and thus the model value is typed differently). - return t.isFunction() && - getArgTypes() == t.getArgTypes() && - getRangeType().isSubtypeOf(t.getRangeType()); + return t.isFunction() && getArgTypes() == t.getArgTypes() && getRangeType().isSubtypeOf(t.getRangeType()); } if(isParametricDatatype() && t.isParametricDatatype()) { Assert(getKind() == kind::PARAMETRIC_DATATYPE); @@ -153,6 +135,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { if(isSet() && t.isSet()) { return getSetElementType().isSubtypeOf(t.getSetElementType()); } + if(isArray() && t.isArray()) { + //reverse for index type + return t.getArrayIndexType().isSubtypeOf(getArrayIndexType()) && + getArrayConstituentType().isSubtypeOf(t.getArrayConstituentType()); + } return false; } @@ -163,39 +150,21 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isSubtypeOf(NodeManager::currentNM()->realType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } - if(isTuple() || isRecord()) { - if(t.isTuple() || t.isRecord()) { - if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { + if(isTuple() && t.isTuple()) { + const Datatype& dt1 = getDatatype(); + const Datatype& dt2 = t.getDatatype(); + if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){ + return false; + } + // r1's fields must be subtypes of r2's, in order + for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){ + if( !dt1[0][i].getRangeType().isComparableTo( dt2[0][i].getRangeType() ) ){ return false; } - if(isTuple()) { - if(getNumChildren() != t.getNumChildren()) { - return false; - } - // children must be comparable to t's, in order - for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { - if(!(*i).isComparableTo(*j)) { - return false; - } - } - } else { - const Record& r1 = getRecord(); - const Record& r2 = t.getRecord(); - if(r1.getNumFields() != r2.getNumFields()) { - return false; - } - // r1's fields must be comparable to r2's, in order - // names must match also - const Record::FieldVector& fields1 = r1.getFields(); - const Record::FieldVector& fields2 = r2.getFields(); - for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) { - if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) { - return false; - } - } - } - return true; } + return true; + //}else if( isRecord() && t.isRecord() ){ + //record types are incomparable in current implementation } else if(isParametricDatatype() && t.isParametricDatatype()) { Assert(getKind() == kind::PARAMETRIC_DATATYPE); Assert(t.getKind() == kind::PARAMETRIC_DATATYPE); @@ -211,10 +180,12 @@ bool TypeNode::isComparableTo(TypeNode t) const { } else if(isSet() && t.isSet()) { return getSetElementType().isComparableTo(t.getSetElementType()); } - - if(isPredicateSubtype()) { - return t.isComparableTo(getSubtypeParentType()); + if(isArray() && t.isArray()) { + return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType()); } + //if(isPredicateSubtype()) { + // return t.isComparableTo(getSubtypeParentType()); + //} return false; } @@ -271,13 +242,13 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { /** Is this a tuple type? */ bool TypeNode::isTuple() const { - return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) || + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) || ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); } /** Is this a record type? */ bool TypeNode::isRecord() const { - return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) ) || + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) || ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); } @@ -294,14 +265,16 @@ vector<TypeNode> TypeNode::getTupleTypes() const { Assert(dt.getNumConstructors()==1); vector<TypeNode> types; for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { - types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType())); + types.push_back(TypeNode::fromType(dt[0][i].getRangeType())); } return types; } const Record& TypeNode::getRecord() const { Assert(isRecord()); - return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); + const Datatype & dt = getDatatype(); + return *(dt.getRecord()); + //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); } vector<TypeNode> TypeNode::getSExprTypes() const { @@ -341,6 +314,14 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { } TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ + return commonTypeNode( t0, t1, true ); +} + +TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ + return commonTypeNode( t0, t1, false ); +} + +TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); @@ -361,65 +342,75 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ return t0; //IntegerType } else if(t1.isReal()) { // t0 == IntegerType && t1.isReal() && !t1.isInteger() - return NodeManager::currentNM()->realType(); // RealType + return isLeast ? t1 : t0; // RealType } else { return TypeNode(); // null type } case REAL_TYPE: if(t1.isReal()) { - return t0; // RealType + return isLeast ? t0 : t1; // RealType } else { return TypeNode(); // null type } default: - if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - return t0; // t0 is a constant type - } else { + //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { + // return t0; // t0 is a constant type + //} else { return TypeNode(); // null type - } + //} } } else if(t1.getKind() == kind::TYPE_CONSTANT) { - return leastCommonTypeNode(t1, t0); // decrease the number of special cases + return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases } // t0 != t1 && // t0.getKind() == kind::TYPE_CONSTANT && // t1.getKind() == kind::TYPE_CONSTANT switch(t0.getKind()) { - case kind::ARRAY_TYPE: case kind::BITVECTOR_TYPE: case kind::SORT_TYPE: case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - return t0; - } else { + //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { + // return t0; + //} else { return TypeNode(); - } + //} case kind::FUNCTION_TYPE: return TypeNode(); // Not sure if this is right case kind::SET_TYPE: { // take the least common subtype of element types TypeNode elementType; - if(t1.isSet() && - ! (elementType = leastCommonTypeNode(t0[0], t1[0])).isNull() ) { + if(t1.isSet() && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull() ) { return NodeManager::currentNM()->mkSetType(elementType); } else { return TypeNode(); } } + case kind::ARRAY_TYPE: { + TypeNode indexType, elementType; + if(t1.isArray() && + ! (indexType = commonTypeNode(t0[0], t1[0], !isLeast)).isNull() && + ! (elementType = commonTypeNode(t0[1], t1[1], isLeast)).isNull() ) { + return NodeManager::currentNM()->mkArrayType(indexType, elementType); + } else { + return TypeNode(); + } + } case kind::SEXPR_TYPE: Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); return TypeNode(); case kind::SUBTYPE_TYPE: - if(t1.isPredicateSubtype()){ - // This is the case where both t0 and t1 are predicate subtypes. - return leastCommonPredicateSubtype(t0, t1); - }else{ // t0 is a predicate subtype and t1 is not - return leastCommonTypeNode(t1, t0); //decrease the number of special cases - } + //if(t1.isPredicateSubtype()){ + // // This is the case where both t0 and t1 are predicate subtypes. + // return leastCommonPredicateSubtype(t0, t1); + //}else{ // t0 is a predicate subtype and t1 is not + // return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases + //} + return TypeNode(); case kind::SUBRANGE_TYPE: + /* if(t1.isSubrange()) { const SubrangeBounds& t0SR = t0.getSubrangeBounds(); const SubrangeBounds& t1SR = t1.getSubrangeBounds(); @@ -449,62 +440,28 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ Assert(t1.isInteger()); return TypeNode(); } -/* - case kind::TUPLE_TYPE: { - // if the other == this one, we returned already, above - if(t0.getBaseType() == t1) { - return t1; - } - if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector<TypeNode> types; - // construct childwise leastCommonType, if one exists - for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) { - TypeNode kid = leastCommonTypeNode(*i, *j); - if(kid.isNull()) { - // no common supertype: types t0, t1 not compatible - return TypeNode(); - } - types.push_back(kid); - } - // if we make it here, we constructed the least common type - return NodeManager::currentNM()->mkTupleType(types); - } - case kind::RECORD_TYPE: { - // if the other == this one, we returned already, above - if(t0.getBaseType() == t1) { - return t1; - } - const Record& r0 = t0.getConst<Record>(); - if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector< std::pair<std::string, Type> > fields; - const Record& r1 = t1.getConst<Record>(); - const Record::FieldVector& fields0 = r0.getFields(); - const Record::FieldVector& fields1 = r1.getFields(); - // construct childwise leastCommonType, if one exists - for(Record::FieldVector::const_iterator i = fields0.begin(), j = fields1.begin(); i != fields0.end(); ++i, ++j) { - TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second)); - if((*i).first != (*j).first || kid.isNull()) { - // if field names differ, or no common supertype, then - // types t0, t1 not compatible - return TypeNode(); - } - fields.push_back(std::make_pair((*i).first, kid.toType())); - } - // if we make it here, we constructed the least common type - return NodeManager::currentNM()->mkRecordType(Record(fields)); - } */ + return TypeNode(); case kind::DATATYPE_TYPE: - // t1 might be a subtype tuple or record - if(t1.getBaseType() == t0) { - return t0; + if( t0.isTuple() && t1.isTuple() ){ + const Datatype& dt1 = t0.getDatatype(); + const Datatype& dt2 = t1.getDatatype(); + if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ + std::vector< TypeNode > lc_types; + for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){ + TypeNode tc = commonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ), isLeast ); + if( tc.isNull() ){ + return tc; + }else{ + lc_types.push_back( tc ); + } + } + return NodeManager::currentNM()->mkTupleType( lc_types ); + } } + //else if( t0.isRecord() && t1.isRecord() ){ + //record types are not related in current implementation + //} // otherwise no common ancestor return TypeNode(); case kind::PARAMETRIC_DATATYPE: { @@ -519,12 +476,12 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ } vector<Type> v; for(size_t i = 1; i < t0.getNumChildren(); ++i) { - v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType()); + v.push_back(commonTypeNode(t0[i], t1[i], isLeast).toType()); } return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v)); } default: - Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); + Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); return TypeNode(); } } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 4c48cc3ca..cfb61a085 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type_node.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tianyi Liang, Kshitij Bansal, Tim King + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Martin Brain ** 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 Reference-counted encapsulation of a pointer to node information. ** @@ -642,8 +642,10 @@ public: * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice */ static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); + static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); private: + static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); /** * Returns the leastUpperBound in the extended type lattice of two diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index bc780a7e5..4874a84b8 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type_properties_template.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Template for the Type properties header ** diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 97bc3ae4b..c88c3b591 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file uninterpreted_constant.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Representation of constants of uninterpreted sorts ** diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 5b2293df6..7d7a3759b 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -1,13 +1,13 @@ /********************* */ /*! \file uninterpreted_constant.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 Representation of constants of uninterpreted sorts ** diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index 59ce5c606..00d2c3eac 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -1,13 +1,13 @@ /********************* */ /*! \file variable_type_map.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** 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 [[ Add one-line brief description here ]] ** |