GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/type_matcher.cpp Lines: 59 62 95.2 %
Date: 2021-03-22 Branches: 84 158 53.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_matcher.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
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 Implementation of a class representing a type matcher
13
 **/
14
15
#include "type_matcher.h"
16
17
namespace CVC4 {
18
19
1765
TypeMatcher::TypeMatcher(TypeNode dt)
20
{
21
1765
  Assert(dt.isDatatype());
22
1765
  addTypesFromDatatype(dt);
23
1765
}
24
25
1859
void TypeMatcher::addTypesFromDatatype(TypeNode dt)
26
{
27
3718
  std::vector<TypeNode> argTypes = dt.getParamTypes();
28
1859
  addTypes(argTypes);
29
1859
  Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
30
4199
  for (unsigned i = 0, narg = argTypes.size(); i < narg; ++i)
31
  {
32
2340
    if (dt.isParameterInstantiatedDatatype(i))
33
    {
34
1564
      Debug("typecheck-idt")
35
782
          << "++ instantiate param " << i << " : " << d_types[i] << std::endl;
36
782
      d_match[i] = d_types[i];
37
    }
38
  }
39
1859
}
40
41
2340
void TypeMatcher::addType(TypeNode t)
42
{
43
2340
  d_types.push_back(t);
44
2340
  d_match.push_back(TypeNode::null());
45
2340
}
46
47
1859
void TypeMatcher::addTypes(const std::vector<TypeNode>& types)
48
{
49
4199
  for (const TypeNode& t : types)
50
  {
51
2340
    addType(t);
52
  }
53
1859
}
54
55
4992
bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn)
56
{
57
9984
  Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn
58
4992
                         << std::endl;
59
  std::vector<TypeNode>::iterator i =
60
4992
      std::find(d_types.begin(), d_types.end(), pattern);
61
4992
  if (i != d_types.end())
62
  {
63
1928
    size_t index = i - d_types.begin();
64
1928
    if (!d_match[index].isNull())
65
    {
66
878
      Debug("typecheck-idt")
67
439
          << "check subtype " << tn << " " << d_match[index] << std::endl;
68
878
      TypeNode tnn = TypeNode::leastCommonTypeNode(tn, d_match[index]);
69
      // recognize subtype relation
70
439
      if (!tnn.isNull())
71
      {
72
439
        d_match[index] = tnn;
73
439
        return true;
74
      }
75
      return false;
76
    }
77
1489
    d_match[index] = tn;
78
1489
    return true;
79
  }
80
3064
  else if (pattern == tn)
81
  {
82
1720
    return true;
83
  }
84
2688
  else if (pattern.getKind() != tn.getKind()
85
1344
           || pattern.getNumChildren() != tn.getNumChildren())
86
  {
87
31
    return false;
88
  }
89
1313
  else if (pattern.getNumChildren() == 0)
90
  {
91
    // fail if the type parameter or type constructors are different
92
    return pattern == tn;
93
  }
94
4188
  for (size_t j = 0, nchild = pattern.getNumChildren(); j < nchild; j++)
95
  {
96
2875
    if (!doMatching(pattern[j], tn[j]))
97
    {
98
      return false;
99
    }
100
  }
101
1313
  return true;
102
}
103
104
521
void TypeMatcher::getTypes(std::vector<TypeNode>& types) const
105
{
106
521
  types.clear();
107
1234
  for (const TypeNode& t : d_types)
108
  {
109
713
    types.push_back(t);
110
  }
111
521
}
112
1619
void TypeMatcher::getMatches(std::vector<TypeNode>& types) const
113
{
114
1619
  types.clear();
115
3654
  for (size_t i = 0, nmatch = d_match.size(); i < nmatch; i++)
116
  {
117
2035
    if (d_match[i].isNull())
118
    {
119
32
      types.push_back(d_types[i]);
120
    }
121
    else
122
    {
123
2003
      types.push_back(d_match[i]);
124
    }
125
  }
126
1619
}
127
128
26676
}  // namespace CVC4