expr_manager_scope.h
expr_stream.h
kind_map.h
- matcher.h
match_trie.cpp
match_trie.h
node.cpp
type.cpp
type.h
type_checker.h
+ type_matcher.cpp
+ type_matcher.h
type_node.cpp
type_node.h
variable_type_map.h
#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"
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();
+++ /dev/null
-/********************* */
-/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#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 {
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();
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)) {
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");
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(
}
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,
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,
#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 {
projects / cvc5.git / commitdiff