GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/type_matcher.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_matcher.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief A class representing a type matcher
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__TYPE_MATCHER_H
18
#define CVC4__EXPR__TYPE_MATCHER_H
19
20
#include <vector>
21
22
#include "expr/type_node.h"
23
24
namespace CVC4 {
25
26
/**
27
 * This class is used for inferring the parameters of an instantiated
28
 * parametric datatype. For example, given parameteric datatype:
29
 *   (par (T) (List T))
30
 * and instantiated parametric datatype (List Int), this class is used to
31
 * infer the mapping { T -> Int }.
32
 */
33
class TypeMatcher
34
{
35
 public:
36
102
  TypeMatcher() {}
37
  /** Initialize this class to do matching with datatype type dt */
38
  TypeMatcher(TypeNode dt);
39
1867
  ~TypeMatcher() {}
40
  /**
41
   * Add the parameter types from datatype type dt to the above vectors,
42
   * initializing d_match to null.
43
   */
44
  void addTypesFromDatatype(TypeNode dt);
45
  /**
46
   * Do matching on type pattern and tn.
47
   * If this method returns true, then tn is an instantiation of parametric
48
   * datatype pattern. The parameters of tn that were inferred are stored in
49
   * d_match such that pattern * { d_types -> d_match } = tn.
50
   */
51
  bool doMatching(TypeNode pattern, TypeNode tn);
52
53
  /** Get the parameter types that this class matched on */
54
  void getTypes(std::vector<TypeNode>& types) const;
55
  /**
56
   * Get the match for the parameter types based on the last call to doMatching.
57
   */
58
  void getMatches(std::vector<TypeNode>& types) const;
59
60
 private:
61
  /** The parameter types */
62
  std::vector<TypeNode> d_types;
63
  /** The types they matched */
64
  std::vector<TypeNode> d_match;
65
  /** Add a parameter type to the above vectors */
66
  void addType(TypeNode t);
67
  /** Add parameter types to the above vectors */
68
  void addTypes(const std::vector<TypeNode>& types);
69
}; /* class TypeMatcher */
70
71
}  // namespace CVC4
72
73
#endif /* CVC4__MATCHER_H */