diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-21 09:26:04 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-21 09:26:19 -0500 |
commit | a33dac29d9cc8520f62b6e4f4f9138ea4e3fbcd4 (patch) | |
tree | b92bc3f34aca16a4b4ed6d42b2c2ae909dff17d4 /src/expr | |
parent | 8a0d2b0577e174d2078026129dd01ea46f7f984a (diff) |
Handle subtypes in sets. Bug fixes for tuples with subtypes.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/type_node.cpp | 40 | ||||
-rw-r--r-- | src/expr/type_node.h | 4 |
2 files changed, 44 insertions, 0 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index f11aa019e..720814aa8 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -539,6 +539,46 @@ TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){ } } + +Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { + TypeNode ntn = n.getType(); + Assert( ntn.isComparableTo( tn ) ); + if( !ntn.isSubtypeOf( tn ) ){ + if( tn.isInteger() ){ + if( tn.isSubtypeOf( ntn ) ){ + return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n ); + } + }else if( tn.isDatatype() && ntn.isDatatype() ){ + if( tn.isTuple() && ntn.isTuple() ){ + const Datatype& dt1 = tn.getDatatype(); + const Datatype& dt2 = ntn.getDatatype(); + if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ + std::vector< Node > conds; + for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){ + Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt2[0][i].getSelector() ), n ); + Node etc = getEnsureTypeCondition( s, TypeNode::fromType( dt1[0][i].getRangeType() ) ); + if( etc.isNull() ){ + return Node::null(); + }else{ + conds.push_back( etc ); + } + } + if( conds.empty() ){ + return NodeManager::currentNM()->mkConst( true ); + }else if( conds.size()==1 ){ + return conds[0]; + }else{ + return NodeManager::currentNM()->mkNode( kind::AND, conds ); + } + } + } + } + return Node::null(); + }else{ + return NodeManager::currentNM()->mkConst( true ); + } +} + /** Is this a sort kind */ bool TypeNode::isSort() const { return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0abbc9a1b..114b8a8ed 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -651,6 +651,10 @@ public: static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); + /** get ensure type condition + * Return value is a condition that implies that n has type tn. + */ + static Node getEnsureTypeCondition( Node n, TypeNode tn ); private: static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); |