GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/type_checker_util.h Lines: 36 48 75.0 %
Date: 2021-03-22 Branches: 164 1478 11.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_checker_util.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli
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 Templates for simple type rules
13
 **
14
 ** This file defines templates for simple type rules. If a kind has the a
15
 ** type rule where each argument matches exactly a specific sort, these
16
 ** templates can be used to define typechecks without writing dedicated classes
17
 ** for them.
18
 **/
19
20
#include "cvc4_private.h"
21
22
#include <sstream>
23
24
#include "expr/kind.h"
25
#include "expr/node.h"
26
#include "expr/node_manager.h"
27
#include "expr/type_node.h"
28
29
namespace CVC4 {
30
namespace expr {
31
32
/** Type check returns the builtin operator sort */
33
struct RBuiltinOperator
34
{
35
4700
  static TypeNode mkType(NodeManager* nm) { return nm->builtinOperatorType(); }
36
};
37
38
/** Type check returns the Boolean sort */
39
struct RBool
40
{
41
877783
  static TypeNode mkType(NodeManager* nm) { return nm->booleanType(); }
42
};
43
44
/** Type check returns the integer sort */
45
struct RInteger
46
{
47
8647
  static TypeNode mkType(NodeManager* nm) { return nm->integerType(); }
48
};
49
50
/** Type check returns the real sort */
51
struct RReal
52
{
53
1950
  static TypeNode mkType(NodeManager* nm) { return nm->realType(); }
54
};
55
56
/** Type check returns the regexp sort */
57
struct RRegExp
58
{
59
29914
  static TypeNode mkType(NodeManager* nm) { return nm->regExpType(); }
60
};
61
62
/** Type check returns the string sort */
63
struct RString
64
{
65
31040
  static TypeNode mkType(NodeManager* nm) { return nm->stringType(); }
66
};
67
68
/** Argument does not exist */
69
struct ANone
70
{
71
1062807
  static bool checkArg(TNode n, size_t arg)
72
  {
73
1062807
    Assert(arg >= n.getNumChildren());
74
1062807
    return true;
75
  }
76
  constexpr static const char* typeName = "<none>";
77
};
78
79
/** Argument is optional */
80
template<class A>
81
struct AOptional
82
{
83
  static bool checkArg(TNode n, size_t arg)
84
  {
85
    if (arg < n.getNumChildren()) {
86
      return A::checkArg(n, arg);
87
    }
88
    return true;
89
  }
90
  constexpr static const char* typeName = A::typeName;
91
};
92
93
/** Argument is an integer */
94
struct AInteger
95
{
96
12832
  static bool checkArg(TNode n, size_t arg)
97
  {
98
25664
    TypeNode t = n[arg].getType(true);
99
25664
    return t.isInteger();
100
  }
101
  constexpr static const char* typeName = "integer";
102
};
103
104
/** Argument is a real */
105
struct AReal
106
{
107
1743965
  static bool checkArg(TNode n, size_t arg)
108
  {
109
3487930
    TypeNode t = n[arg].getType(true);
110
3487930
    return t.isReal();
111
  }
112
  constexpr static const char* typeName = "real";
113
};
114
115
/** Argument is a regexp */
116
struct ARegExp
117
{
118
19861
  static bool checkArg(TNode n, size_t arg)
119
  {
120
39722
    TypeNode t = n[arg].getType(true);
121
39722
    return t.isRegExp();
122
  }
123
  constexpr static const char* typeName = "regexp";
124
};
125
126
/** Argument is a string */
127
struct AString
128
{
129
17660
  static bool checkArg(TNode n, size_t arg)
130
  {
131
35320
    TypeNode t = n[arg].getType(true);
132
35320
    return t.isString();
133
  }
134
  constexpr static const char* typeName = "string";
135
};
136
137
/**
138
 * The SimpleTypeRule template can be used to obtain a simple type rule by
139
 * defining a return type and the argument types (up to three arguments are
140
 * supported).
141
 * */
142
template <class R, class A0 = ANone, class A1 = ANone, class A2 = ANone>
143
class SimpleTypeRule
144
{
145
 public:
146
951941
  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
147
  {
148
951941
    if (check)
149
    {
150
950375
      if (!A0::checkArg(n, 0))
151
      {
152
4
        std::stringstream msg;
153
2
        msg << "Expecting a " << A0::typeName
154
2
            << " term as the first argument in '" << n.getKind() << "'";
155
2
        throw TypeCheckingExceptionPrivate(n, msg.str());
156
      }
157
950373
      if (!A1::checkArg(n, 1))
158
      {
159
        std::stringstream msg;
160
        msg << "Expecting a " << A1::typeName
161
            << " term as the second argument in '" << n.getKind() << "'";
162
        throw TypeCheckingExceptionPrivate(n, msg.str());
163
      }
164
950373
      if (!A2::checkArg(n, 2))
165
      {
166
        std::stringstream msg;
167
        msg << "Expecting a " << A2::typeName
168
            << " term as the third argument in '" << n.getKind() << "'";
169
        throw TypeCheckingExceptionPrivate(n, msg.str());
170
      }
171
    }
172
951939
    return R::mkType(nm);
173
  }
174
};
175
176
/**
177
 * The SimpleTypeRuleVar template can be used to obtain a simple type rule for
178
 * operators with a variable number of arguments. It takes the return type and
179
 * the type of the arguments as template parameters.
180
 * */
181
template <class R, class A>
182
class SimpleTypeRuleVar
183
{
184
 public:
185
2095
  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
186
  {
187
2095
    if (check)
188
    {
189
8099
      for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
190
      {
191
6004
        if (!A::checkArg(n, i))
192
        {
193
          std::stringstream msg;
194
          msg << "Expecting a " << A::typeName << " term as argument " << i
195
              << " in '" << n.getKind() << "'";
196
          throw TypeCheckingExceptionPrivate(n, msg.str());
197
        }
198
      }
199
    }
200
2095
    return R::mkType(nm);
201
  }
202
};
203
204
}  // namespace expr
205
}  // namespace CVC4