From: Andrew Reynolds Date: Thu, 29 Nov 2012 22:02:20 +0000 (+0000) Subject: fixes bug 438, incorporate subtypes into type unification when typechecking parameter... X-Git-Tag: cvc5-1.0.0~7528 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7bb97d7258303c5ac228222baccb6bffe3c55f50;p=cvc5.git fixes bug 438, incorporate subtypes into type unification when typechecking parameterized datatypes --- diff --git a/src/util/matcher.h b/src/util/matcher.h index 1eb722978..78738e27f 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -66,8 +66,16 @@ public: std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern ); if( i!=d_types.end() ){ int index = i - d_types.begin(); - if( !d_match[index].isNull() && d_match[index]!=tn ){ - return false; + if( !d_match[index].isNull() ){ + Debug("typecheck-idt") << "check subtype " << tn << " " << d_match[index] << std::endl; + TypeNode tnn = TypeNode::leastCommonTypeNode( tn, d_match[index] ); + //recognize subtype relation + if( !tnn.isNull() ){ + d_match[index] = tnn; + return true; + }else{ + return false; + } }else{ d_match[ i - d_types.begin() ] = tn; return true;