GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/theory_arith_type_rules.h Lines: 44 59 74.6 %
Date: 2021-03-22 Branches: 57 183 31.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arith_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Dejan Jovanovic
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__ARITH__THEORY_ARITH_TYPE_RULES_H
20
#define CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
26
27
class ArithConstantTypeRule {
28
public:
29
235981
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
30
  {
31
235981
    Assert(n.getKind() == kind::CONST_RATIONAL);
32
235981
    if(n.getConst<Rational>().isIntegral()){
33
108694
      return nodeManager->integerType();
34
    }else{
35
127287
      return nodeManager->realType();
36
    }
37
  }
38
};/* class ArithConstantTypeRule */
39
40
class ArithOperatorTypeRule {
41
public:
42
3476319
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
43
  {
44
6952638
    TypeNode integerType = nodeManager->integerType();
45
6952638
    TypeNode realType = nodeManager->realType();
46
3476319
    TNode::iterator child_it = n.begin();
47
3476319
    TNode::iterator child_it_end = n.end();
48
3476319
    bool isInteger = true;
49
20754571
    for(; child_it != child_it_end; ++child_it) {
50
17278252
      TypeNode childType = (*child_it).getType(check);
51
8639126
      if (!childType.isInteger()) {
52
1526722
        isInteger = false;
53
1526722
        if( !check ) { // if we're not checking, nothing left to do
54
          break;
55
        }
56
      }
57
8639126
      if( check ) {
58
8639126
        if(!childType.isReal()) {
59
          throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
60
        }
61
      }
62
    }
63
3476319
    switch (Kind k = n.getKind())
64
    {
65
1528
      case kind::TO_REAL:
66
1528
      case kind::CAST_TO_REAL: return realType;
67
293
      case kind::TO_INTEGER: return integerType;
68
3474498
      default:
69
      {
70
3474498
        bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
71
3474498
        return (isInteger && !isDivision ? integerType : realType);
72
      }
73
    }
74
  }
75
};/* class ArithOperatorTypeRule */
76
77
class RealNullaryOperatorTypeRule {
78
public:
79
1419
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
80
  {
81
    // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation
82
1419
    Assert(check);
83
1419
    TypeNode realType = n.getType();
84
1419
    if(realType!=NodeManager::currentNM()->realType()) {
85
      throw TypeCheckingExceptionPrivate(n, "expecting real type");
86
    }
87
1419
    return realType;
88
  }
89
};/* class RealNullaryOperatorTypeRule */
90
91
class IAndOpTypeRule
92
{
93
 public:
94
61
  inline static TypeNode computeType(NodeManager* nodeManager,
95
                                     TNode n,
96
                                     bool check)
97
  {
98
61
    if (n.getKind() != kind::IAND_OP)
99
    {
100
      InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
101
    }
102
122
    TypeNode iType = nodeManager->integerType();
103
122
    std::vector<TypeNode> argTypes;
104
61
    argTypes.push_back(iType);
105
61
    argTypes.push_back(iType);
106
122
    return nodeManager->mkFunctionType(argTypes, iType);
107
  }
108
}; /* class IAndOpTypeRule */
109
110
class IAndTypeRule
111
{
112
 public:
113
259
  inline static TypeNode computeType(NodeManager* nodeManager,
114
                                     TNode n,
115
                                     bool check)
116
  {
117
259
    if (n.getKind() != kind::IAND)
118
    {
119
      InternalError() << "IAND typerule invoked for IAND kind";
120
    }
121
259
    if (check)
122
    {
123
518
      TypeNode arg1 = n[0].getType(check);
124
518
      TypeNode arg2 = n[1].getType(check);
125
259
      if (!arg1.isInteger() || !arg2.isInteger())
126
      {
127
        throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
128
      }
129
    }
130
259
    return nodeManager->integerType();
131
  }
132
}; /* class BitVectorConversionTypeRule */
133
134
class IndexedRootPredicateTypeRule
135
{
136
 public:
137
  inline static TypeNode computeType(NodeManager* nodeManager,
138
                                     TNode n,
139
                                     bool check)
140
  {
141
    if (check)
142
    {
143
      TypeNode t1 = n[0].getType(check);
144
      if (!t1.isBoolean())
145
      {
146
        throw TypeCheckingExceptionPrivate(
147
            n, "expecting boolean term as first argument");
148
      }
149
      TypeNode t2 = n[1].getType(check);
150
      if (!t2.isReal())
151
      {
152
        throw TypeCheckingExceptionPrivate(
153
            n, "expecting polynomial as second argument");
154
      }
155
    }
156
    return nodeManager->booleanType();
157
  }
158
}; /* class IndexedRootPredicateTypeRule */
159
160
}/* CVC4::theory::arith namespace */
161
}/* CVC4::theory namespace */
162
}/* CVC4 namespace */
163
164
#endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */