diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
tree | dc4b56e27701abd61ebd69675f86a9366d90998f /src/expr | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_builder.h | 14 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 54 |
3 files changed, 59 insertions, 11 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5159f6b5a..eab41ee38 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -936,7 +936,7 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr ("export of types belonging to theory of DATATYPES kinds unsupported"); } if(n.getMetaKind() == kind::metakind::PARAMETERIZED && - n.getKind() != kind::SORT_TYPE) { + n.getKind() != kind::SORT_TYPE) { throw ExportUnsupportedException ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5f813dbe8..bd3827f47 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -713,6 +713,10 @@ public: operator Node(); operator Node() const; + // similarly for TypeNode + operator TypeNode(); + operator TypeNode() const; + NodeBuilder<nchild_thresh>& operator&=(TNode); NodeBuilder<nchild_thresh>& operator|=(TNode); NodeBuilder<nchild_thresh>& operator+=(TNode); @@ -902,6 +906,16 @@ NodeBuilder<nchild_thresh>::operator Node() const { } template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator TypeNode() { + return constructTypeNode(); +} + +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator TypeNode() const { + return constructTypeNode(); +} + +template <unsigned nchild_thresh> expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 236f48017..7522b8110 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -94,15 +94,32 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { return true; } - if(isTuple() != t.isTuple() || isRecord() != t.isRecord() || - getNumChildren() != t.getNumChildren()) { + if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { 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)) { + if(isTuple()) { + if(getNumChildren() != t.getNumChildren()) { 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 = getConst<Record>(); + const Record& r2 = t.getConst<Record>(); + if(r1.getNumFields() != r2.getNumFields()) { + return false; + } + // r1's fields must be subtypes of r2's, in order + // names must match also + for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) { + if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) { + return false; + } + } } return true; } @@ -125,15 +142,32 @@ bool TypeNode::isComparableTo(TypeNode t) const { NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { return true; } - if(isTuple() != t.isTuple() || isRecord() != t.isRecord() || - getNumChildren() != t.getNumChildren()) { + if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { 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)) { + 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 = getConst<Record>(); + const Record& r2 = t.getConst<Record>(); + if(r1.getNumFields() != r2.getNumFields()) { return false; } + // r1's fields must be comparable to r2's, in order + // names must match also + for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) { + if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) { + return false; + } + } } return true; } else { |