Refactor type matcher utility (#3439)

7 files changed, 218 insertions, 139 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index cae23054c..479b28cfb 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -15,7 +15,6 @@ libcvc4_add_sources(
   expr_manager_scope.h
   expr_stream.h
   kind_map.h
-  matcher.h
   match_trie.cpp
   match_trie.h
   node.cpp
@@ -40,6 +39,8 @@ libcvc4_add_sources(
   type.cpp
   type.h
   type_checker.h
+  type_matcher.cpp
+  type_matcher.h
   type_node.cpp
   type_node.h
   variable_type_map.h
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 2edb1f53b..c09b92cfe 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -23,11 +23,11 @@
 #include "expr/attribute.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
-#include "expr/matcher.h"
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
 #include "expr/node_manager.h"
 #include "expr/type.h"
+#include "expr/type_matcher.h"
 #include "options/datatypes_options.h"
 #include "options/set_language.h"
 #include "theory/type_enumerator.h"
@@ -935,9 +935,9 @@ Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
   ExprManagerScope ems(d_constructor);
   const Datatype& dt = Datatype::datatypeOf(d_constructor);
   PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
-  DatatypeType dtt = dt.getDatatypeType();
-  Matcher m(dtt);
-  m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
+  TypeNode dtt = TypeNode::fromType(dt.getDatatypeType());
+  TypeMatcher m(dtt);
+  m.doMatching(dtt, TypeNode::fromType(returnType));
   vector<Type> subst;
   m.getMatches(subst);
   vector<Type> params = dt.getParameters();
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
deleted file mode 100644
index 9a2dad7d0..000000000
--- a/src/expr/matcher.h
+++ /dev/null
@@ -1,118 +0,0 @@
-/*********************                                                        */
-/*! \file matcher.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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
- **
- ** A class representing a type matcher.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__MATCHER_H
-#define CVC4__MATCHER_H
-
-#include <iosfwd>
-#include <string>
-#include <vector>
-#include <map>
-
-#include "expr/node.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-
-class Matcher {
-private:
-  std::vector< TypeNode > d_types;
-  std::vector< TypeNode > d_match;
-public:
-  Matcher(){}
-  Matcher( DatatypeType dt ){
-    addTypesFromDatatype( dt );
-  }
-  ~Matcher(){}
-
-  void addTypesFromDatatype( DatatypeType dt ){
-    std::vector< Type > argTypes = dt.getParamTypes();
-    addTypes( argTypes );
-    Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
-    for(unsigned i = 0; i < argTypes.size(); ++i) {
-      if(dt.isParameterInstantiated(i)) {
-        Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl;
-        d_match[i] = d_types[i];
-      }
-    }
-  }
-  void addType( Type t ){
-    d_types.push_back( TypeNode::fromType( t ) );
-    d_match.push_back( TypeNode::null() );
-  }
-  void addTypes( std::vector< Type > types ){
-    for( int i=0; i<(int)types.size(); i++ ){
-      addType( types[i] );
-    }
-  }
-
-  bool doMatching( TypeNode pattern, TypeNode tn ){
-    Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn << std::endl;
-    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() ){
-        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;
-      }
-    }else if( pattern==tn ){
-      return true;
-    }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){
-      return false;
-    }else{
-      for( int i=0; i<(int)pattern.getNumChildren(); i++ ){
-        if( !doMatching( pattern[i], tn[i] ) ){
-          return false;
-        }
-      }
-      return true;
-    }
-  }
-
-  TypeNode getMatch( unsigned int i ){ return d_match[i]; }
-  void getTypes( std::vector<Type>& types ) {
-    types.clear();
-    for( int i=0; i<(int)d_match.size(); i++ ){
-      types.push_back( d_types[i].toType() );
-    }
-  }
-  void getMatches( std::vector<Type>& types ) {
-    types.clear();
-    for( int i=0; i<(int)d_match.size(); i++ ){
-      if(d_match[i].isNull()) {
-        types.push_back( d_types[i].toType() );
-      } else {
-        types.push_back( d_match[i].toType() );
-      }
-    }
-  }
-};/* class Matcher */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__MATCHER_H */
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
new file mode 100644
index 000000000..a21dc2cc0
--- /dev/null
+++ b/src/expr/type_matcher.cpp
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \file type_matcher.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 a class representing a type matcher
+ **/
+
+#include "type_matcher.h"
+
+namespace CVC4 {
+
+TypeMatcher::TypeMatcher(TypeNode dt)
+{
+  Assert(dt.isDatatype());
+  addTypesFromDatatype(dt);
+}
+
+void TypeMatcher::addTypesFromDatatype(TypeNode dt)
+{
+  std::vector<TypeNode> argTypes = dt.getParamTypes();
+  addTypes(argTypes);
+  Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
+  for (unsigned i = 0, narg = argTypes.size(); i < narg; ++i)
+  {
+    if (dt.isParameterInstantiatedDatatype(i))
+    {
+      Debug("typecheck-idt")
+          << "++ instantiate param " << i << " : " << d_types[i] << std::endl;
+      d_match[i] = d_types[i];
+    }
+  }
+}
+
+void TypeMatcher::addType(TypeNode t)
+{
+  d_types.push_back(t);
+  d_match.push_back(TypeNode::null());
+}
+
+void TypeMatcher::addTypes(const std::vector<TypeNode>& types)
+{
+  for (const TypeNode& t : types)
+  {
+    addType(t);
+  }
+}
+
+bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn)
+{
+  Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn
+                         << std::endl;
+  std::vector<TypeNode>::iterator i =
+      std::find(d_types.begin(), d_types.end(), pattern);
+  if (i != d_types.end())
+  {
+    size_t index = i - d_types.begin();
+    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;
+      }
+      return false;
+    }
+    d_match[index] = tn;
+    return true;
+  }
+  else if (pattern == tn)
+  {
+    return true;
+  }
+  else if (pattern.getKind() != tn.getKind()
+           || pattern.getNumChildren() != tn.getNumChildren())
+  {
+    return false;
+  }
+  for (size_t i = 0, nchild = pattern.getNumChildren(); i < nchild; i++)
+  {
+    if (!doMatching(pattern[i], tn[i]))
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+void TypeMatcher::getTypes(std::vector<Type>& types)
+{
+  types.clear();
+  for (TypeNode& t : d_types)
+  {
+    types.push_back(t.toType());
+  }
+}
+void TypeMatcher::getMatches(std::vector<Type>& types)
+{
+  types.clear();
+  for (size_t i = 0, nmatch = d_match.size(); i < nmatch; i++)
+  {
+    if (d_match[i].isNull())
+    {
+      types.push_back(d_types[i].toType());
+    }
+    else
+    {
+      types.push_back(d_match[i].toType());
+    }
+  }
+}
+
+}  // namespace CVC4
diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
new file mode 100644
index 000000000..778338df7
--- /dev/null
+++ b/src/expr/type_matcher.h
@@ -0,0 +1,74 @@
+/*********************                                                        */
+/*! \file type_matcher.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__TYPE_MATCHER_H
+#define CVC4__EXPR__TYPE_MATCHER_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+/**
+ * This class is used for inferring the parameters of an instantiated
+ * parametric datatype. For example, given parameteric datatype:
+ *   (par (T) (List T))
+ * and instantiated parametric datatype (List Int), this class is used to
+ * infer the mapping { T -> Int }.
+ */
+class TypeMatcher
+{
+ public:
+  TypeMatcher() {}
+  /** Initialize this class to do matching with datatype type dt */
+  TypeMatcher(TypeNode dt);
+  ~TypeMatcher() {}
+  /**
+   * Add the parameter types from datatype type dt to the above vectors,
+   * initializing d_match to null.
+   */
+  void addTypesFromDatatype(TypeNode dt);
+  /**
+   * Do matching on type pattern and tn.
+   * If this method returns true, then tn is an instantiation of parametric
+   * datatype pattern. The parameters of tn that were inferred are stored in
+   * d_match such that pattern * { d_types -> d_match } = tn.
+   */
+  bool doMatching(TypeNode pattern, TypeNode tn);
+
+  /** Get the parameter types that this class matched on */
+  void getTypes(std::vector<Type>& types);
+  /**
+   * Get the match for the parameter types based on the last call to doMatching.
+   */
+  void getMatches(std::vector<Type>& types);
+
+ private:
+  /** The parameter types */
+  std::vector<TypeNode> d_types;
+  /** The types they matched */
+  std::vector<TypeNode> d_match;
+  /** Add a parameter type to the above vectors */
+  void addType(TypeNode t);
+  /** Add parameter types to the above vectors */
+  void addTypes(const std::vector<TypeNode>& types);
+}; /* class TypeMatcher */
+
+}  // namespace CVC4
+
+#endif /* CVC4__MATCHER_H */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index c28673321..566fa47aa 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -19,8 +19,7 @@
 #ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
-#include "expr/matcher.h"
-//#include "expr/attribute.h"
+#include "expr/type_matcher.h"
 
 namespace CVC4 {
 
@@ -41,9 +40,9 @@ struct DatatypeConstructorTypeRule {
                                      bool check) {
     Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
     TypeNode consType = n.getOperator().getType(check);
-    Type t = consType.getConstructorRangeType().toType();
+    TypeNode t = consType.getConstructorRangeType();
     Assert(t.isDatatype());
-    DatatypeType dt = DatatypeType(t);
+    DatatypeType dt = DatatypeType(t.toType());
     TNode::iterator child_it = n.begin();
     TNode::iterator child_it_end = n.end();
     TypeNode::iterator tchild_it = consType.begin();
@@ -55,7 +54,7 @@ struct DatatypeConstructorTypeRule {
     if (dt.isParametric()) {
       Debug("typecheck-idt") << "typecheck parameterized datatype " << n
                              << std::endl;
-      Matcher m(dt);
+      TypeMatcher m(t);
       for (; child_it != child_it_end; ++child_it, ++tchild_it) {
         TypeNode childType = (*child_it).getType(check);
         if (!m.doMatching(*tchild_it, childType)) {
@@ -127,9 +126,9 @@ struct DatatypeSelectorTypeRule {
     Assert(n.getKind() == kind::APPLY_SELECTOR
            || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
     TypeNode selType = n.getOperator().getType(check);
-    Type t = selType[0].toType();
+    TypeNode t = selType[0];
     Assert(t.isDatatype());
-    DatatypeType dt = DatatypeType(t);
+    DatatypeType dt = DatatypeType(t.toType());
     if ((dt.isParametric() || check) && n.getNumChildren() != 1) {
       throw TypeCheckingExceptionPrivate(
           n, "number of arguments does not match the selector type");
@@ -137,7 +136,7 @@ struct DatatypeSelectorTypeRule {
     if (dt.isParametric()) {
       Debug("typecheck-idt") << "typecheck parameterized sel: " << n
                              << std::endl;
-      Matcher m(dt);
+      TypeMatcher m(t);
       TypeNode childType = n[0].getType(check);
       if (!childType.isInstantiatedDatatype()) {
         throw TypeCheckingExceptionPrivate(
@@ -183,13 +182,13 @@ struct DatatypeTesterTypeRule {
       }
       TypeNode testType = n.getOperator().getType(check);
       TypeNode childType = n[0].getType(check);
-      Type t = testType[0].toType();
+      TypeNode t = testType[0];
       Assert(t.isDatatype());
-      DatatypeType dt = DatatypeType(t);
+      DatatypeType dt = DatatypeType(t.toType());
       if (dt.isParametric()) {
         Debug("typecheck-idt") << "typecheck parameterized tester: " << n
                                << std::endl;
-        Matcher m(dt);
+        TypeMatcher m(t);
         if (!m.doMatching(testType[0], childType)) {
           throw TypeCheckingExceptionPrivate(
               n,
@@ -217,12 +216,11 @@ struct DatatypeAscriptionTypeRule {
     if (check) {
       TypeNode childType = n[0].getType(check);
 
-      Matcher m;
+      TypeMatcher m;
       if (childType.getKind() == kind::CONSTRUCTOR_TYPE) {
-        m.addTypesFromDatatype(
-            ConstructorType(childType.toType()).getRangeType());
+        m.addTypesFromDatatype(childType.getConstructorRangeType());
       } else if (childType.getKind() == kind::DATATYPE_TYPE) {
-        m.addTypesFromDatatype(DatatypeType(childType.toType()));
+        m.addTypesFromDatatype(childType);
       }
       if (!m.doMatching(childType, t)) {
         throw TypeCheckingExceptionPrivate(n,
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 62d75cf18..a83dbf541 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -19,7 +19,8 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
 #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
 
-#include "expr/matcher.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {