GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/theory_bool_type_rules.h Lines: 29 29 100.0 %
Date: 2021-03-22 Branches: 75 140 53.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bool_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Morgan Deters, Christopher L. Conway
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_BOOL_TYPE_RULES_H
20
#define CVC4__THEORY_BOOL_TYPE_RULES_H
21
22
namespace CVC4 {
23
namespace theory {
24
namespace boolean {
25
26
class BooleanTypeRule {
27
public:
28
11281446
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
29
  {
30
11281446
    TypeNode booleanType = nodeManager->booleanType();
31
11281446
    if( check ) {
32
11280980
      TNode::iterator child_it = n.begin();
33
11280980
      TNode::iterator child_it_end = n.end();
34
90190220
      for(; child_it != child_it_end; ++child_it) {
35
39454946
        if(!(*child_it).getType(check).isBoolean()) {
36
326
          Debug("pb") << "failed type checking: " << *child_it << std::endl;
37
326
          Debug("pb") << "  integer: " << (*child_it).getType(check).isInteger() << std::endl;
38
326
          Debug("pb") << "  real: " << (*child_it).getType(check).isReal() << std::endl;
39
326
          throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression");
40
        }
41
      }
42
    }
43
11281120
    return booleanType;
44
  }
45
};/* class BooleanTypeRule */
46
47
class IteTypeRule {
48
public:
49
1787527
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
50
  {
51
3575054
    TypeNode thenType = n[1].getType(check);
52
3575054
    TypeNode elseType = n[2].getType(check);
53
1787527
    TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
54
1787527
    if( check ) {
55
3575054
      TypeNode booleanType = nodeManager->booleanType();
56
1787527
      if (n[0].getType(check) != booleanType) {
57
24
        throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
58
      }
59
1787503
      if (iteType.isNull()) {
60
16
        std::stringstream ss;
61
8
        ss << "Both branches of the ITE must be a subtype of a common type." << std::endl
62
16
           << "then branch: " << n[1] << std::endl
63
8
           << "its type   : " << thenType << std::endl
64
16
           << "else branch: " << n[2] << std::endl
65
8
           << "its type   : " << elseType << std::endl;
66
8
        throw TypeCheckingExceptionPrivate(n, ss.str());
67
      }
68
    }
69
3574990
    return iteType;
70
  }
71
};/* class IteTypeRule */
72
73
}/* CVC4::theory::boolean namespace */
74
}/* CVC4::theory namespace */
75
}/* CVC4 namespace */
76
77
#endif /* CVC4__THEORY_BOOL_TYPE_RULES_H */