From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
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;