From 911d570a2546a6c90387500f7fa6b1dc3eb045be Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 5 Nov 2019 14:12:43 -0600 Subject: [PATCH] Refactor type matcher utility (#3439) --- src/expr/CMakeLists.txt | 3 +- src/expr/datatype.cpp | 8 +- src/expr/matcher.h | 118 ----------------- src/expr/type_matcher.cpp | 123 ++++++++++++++++++ src/expr/type_matcher.h | 74 +++++++++++ .../datatypes/theory_datatypes_type_rules.h | 28 ++-- .../theory_quantifiers_type_rules.h | 3 +- 7 files changed, 218 insertions(+), 139 deletions(-) delete mode 100644 src/expr/matcher.h create mode 100644 src/expr/type_matcher.cpp create mode 100644 src/expr/type_matcher.h 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 subst; m.getMatches(subst); vector 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 -#include -#include -#include - -#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& types ) { - types.clear(); - for( int i=0; i<(int)d_match.size(); i++ ){ - types.push_back( d_types[i].toType() ); - } - } - void getMatches( std::vector& 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 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& 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::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& types) +{ + types.clear(); + for (TypeNode& t : d_types) + { + types.push_back(t.toType()); + } +} +void TypeMatcher::getMatches(std::vector& 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 + +#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& types); + /** + * Get the match for the parameter types based on the last call to doMatching. + */ + void getMatches(std::vector& types); + + private: + /** The parameter types */ + std::vector d_types; + /** The types they matched */ + std::vector 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& 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 { -- 2.30.2