GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/theory_uf_type_rules.h Lines: 50 74 67.6 %
Date: 2021-03-22 Branches: 86 314 27.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_uf_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 [[ Add brief comments here ]]
13
 **
14
 ** [[ Add file-specific comments here ]]
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
20
#define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
21
22
#include <climits>
23
24
namespace CVC4 {
25
namespace theory {
26
namespace uf {
27
28
class UfTypeRule {
29
 public:
30
452405
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
31
                                     bool check) {
32
904810
    TNode f = n.getOperator();
33
904810
    TypeNode fType = f.getType(check);
34
452405
    if (!fType.isFunction()) {
35
      throw TypeCheckingExceptionPrivate(
36
          n, "operator does not have function type");
37
    }
38
452405
    if (check) {
39
452405
      if (n.getNumChildren() != fType.getNumChildren() - 1) {
40
        throw TypeCheckingExceptionPrivate(
41
            n, "number of arguments does not match the function type");
42
      }
43
452405
      TNode::iterator argument_it = n.begin();
44
452405
      TNode::iterator argument_it_end = n.end();
45
452405
      TypeNode::iterator argument_type_it = fType.begin();
46
14275637
      for (; argument_it != argument_it_end;
47
           ++argument_it, ++argument_type_it) {
48
13823232
        TypeNode currentArgument = (*argument_it).getType();
49
13823232
        TypeNode currentArgumentType = *argument_type_it;
50
6911616
        if (!currentArgument.isSubtypeOf(currentArgumentType)) {
51
          std::stringstream ss;
52
          ss << "argument type is not a subtype of the function's argument "
53
             << "type:\n"
54
             << "argument:  " << *argument_it << "\n"
55
             << "has type:  " << (*argument_it).getType() << "\n"
56
             << "not subtype: " << *argument_type_it << "\n"
57
             << "in term : " << n;
58
          throw TypeCheckingExceptionPrivate(n, ss.str());
59
        }
60
      }
61
    }
62
904810
    return fType.getRangeType();
63
  }
64
}; /* class UfTypeRule */
65
66
class CardinalityConstraintTypeRule {
67
 public:
68
1038
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
69
                                     bool check) {
70
1038
    if (check) {
71
      // don't care what it is, but it should be well-typed
72
1038
      n[0].getType(check);
73
74
2076
      TypeNode valType = n[1].getType(check);
75
1038
      if (valType != nodeManager->integerType()) {
76
        throw TypeCheckingExceptionPrivate(
77
            n, "cardinality constraint must be integer");
78
      }
79
1038
      if (n[1].getKind() != kind::CONST_RATIONAL) {
80
        throw TypeCheckingExceptionPrivate(
81
            n, "cardinality constraint must be a constant");
82
      }
83
2076
      CVC4::Rational r(INT_MAX);
84
1038
      if (n[1].getConst<Rational>() > r) {
85
        throw TypeCheckingExceptionPrivate(
86
            n, "Exceeded INT_MAX in cardinality constraint");
87
      }
88
1038
      if (n[1].getConst<Rational>().getNumerator().sgn() != 1) {
89
        throw TypeCheckingExceptionPrivate(
90
            n, "cardinality constraint must be positive");
91
      }
92
    }
93
1038
    return nodeManager->booleanType();
94
  }
95
}; /* class CardinalityConstraintTypeRule */
96
97
class CombinedCardinalityConstraintTypeRule {
98
 public:
99
587
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
100
                                     bool check) {
101
587
    if (check) {
102
1174
      TypeNode valType = n[0].getType(check);
103
587
      if (valType != nodeManager->integerType()) {
104
        throw TypeCheckingExceptionPrivate(
105
            n, "combined cardinality constraint must be integer");
106
      }
107
587
      if (n[0].getKind() != kind::CONST_RATIONAL) {
108
        throw TypeCheckingExceptionPrivate(
109
            n, "combined cardinality constraint must be a constant");
110
      }
111
1174
      CVC4::Rational r(INT_MAX);
112
587
      if (n[0].getConst<Rational>() > r) {
113
        throw TypeCheckingExceptionPrivate(
114
            n, "Exceeded INT_MAX in combined cardinality constraint");
115
      }
116
587
      if (n[0].getConst<Rational>().getNumerator().sgn() == -1) {
117
        throw TypeCheckingExceptionPrivate(
118
            n, "combined cardinality constraint must be non-negative");
119
      }
120
    }
121
587
    return nodeManager->booleanType();
122
  }
123
}; /* class CardinalityConstraintTypeRule */
124
125
class PartialTypeRule {
126
 public:
127
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
128
                                     bool check) {
129
    return n.getOperator().getType().getRangeType();
130
  }
131
}; /* class PartialTypeRule */
132
133
class CardinalityValueTypeRule {
134
 public:
135
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
136
                                     bool check) {
137
    if (check) {
138
      n[0].getType(check);
139
    }
140
    return nodeManager->integerType();
141
  }
142
}; /* class CardinalityValueTypeRule */
143
144
// class with the typing rule for HO_APPLY terms
145
class HoApplyTypeRule {
146
 public:
147
  // the typing rule for HO_APPLY terms
148
14925
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
149
                                     bool check) {
150
14925
    Assert(n.getKind() == kind::HO_APPLY);
151
29850
    TypeNode fType = n[0].getType(check);
152
14925
    if (!fType.isFunction()) {
153
      throw TypeCheckingExceptionPrivate(
154
          n, "first argument does not have function type");
155
    }
156
14925
    Assert(fType.getNumChildren() >= 2);
157
14925
    if (check) {
158
29850
      TypeNode aType = n[1].getType(check);
159
14925
      if( !aType.isSubtypeOf( fType[0] ) ){
160
        throw TypeCheckingExceptionPrivate(
161
            n, "argument does not match function type");
162
      }
163
    }
164
14925
    if( fType.getNumChildren()==2 ){
165
7119
      return fType.getRangeType();
166
    }else{
167
15612
      std::vector< TypeNode > children;
168
7806
      TypeNode::iterator argument_type_it = fType.begin();
169
7806
      TypeNode::iterator argument_type_it_end = fType.end();
170
7806
      ++argument_type_it;
171
43292
      for (; argument_type_it != argument_type_it_end; ++argument_type_it) {
172
17743
        children.push_back( *argument_type_it );
173
      }
174
7806
      return nodeManager->mkFunctionType( children );
175
    }
176
  }
177
}; /* class HoApplyTypeRule */
178
179
} /* CVC4::theory::uf namespace */
180
} /* CVC4::theory namespace */
181
} /* CVC4 namespace */
182
183
#endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */