diff options
Diffstat (limited to 'src/expr/matcher.h')
-rw-r--r-- | src/expr/matcher.h | 119 |
1 files changed, 119 insertions, 0 deletions
diff --git a/src/expr/matcher.h b/src/expr/matcher.h new file mode 100644 index 000000000..92b1ce109 --- /dev/null +++ b/src/expr/matcher.h @@ -0,0 +1,119 @@ +/********************* */ +/*! \file matcher.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** 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 <iostream> +#include <string> +#include <vector> +#include <map> + +#include "base/cvc4_assert.h" +#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 */ |