1 /********************* */
2 /*! \file theory_bool_type_rules.h
4 ** Original author: dejan
5 ** Major contributors: mdeters, cconway
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add brief comments here ]]
16 ** [[ Add file-specific comments here ]]
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H_
22 #define __CVC4__THEORY_BOOL_TYPE_RULES_H_
28 class BooleanTypeRule
{
30 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
31 throw (TypeCheckingExceptionPrivate
) {
32 TypeNode booleanType
= nodeManager
->booleanType();
34 TNode::iterator child_it
= n
.begin();
35 TNode::iterator child_it_end
= n
.end();
36 for(; child_it
!= child_it_end
; ++child_it
) {
37 if((*child_it
).getType(check
) != booleanType
) {
38 throw TypeCheckingExceptionPrivate(n
, "expecting a Boolean subexpression");
48 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
49 throw (TypeCheckingExceptionPrivate
) {
50 TypeNode iteType
= n
[1].getType(check
);
52 TypeNode booleanType
= nodeManager
->booleanType();
53 if (n
[0].getType(check
) != booleanType
) {
54 throw TypeCheckingExceptionPrivate(n
, "condition of ITE is not Boolean");
56 if (iteType
!= n
[2].getType(check
)) {
57 throw TypeCheckingExceptionPrivate(n
, "both branches of the ITE must be of the same type");
64 } // boolean namespace
68 #endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H_ */