src/theory/booleans/theory_bool_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_bool_type_rules.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief [[ Add brief comments here ]]
  15  **
  16  ** [[ Add file-specific comments here ]]
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H_
  22 #define __CVC4__THEORY_BOOL_TYPE_RULES_H_
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace boolean {
  27
  28 class BooleanTypeRule {
  29 public:
  30   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  31       throw (TypeCheckingExceptionPrivate) {
  32     TypeNode booleanType = nodeManager->booleanType();
  33     if( check ) {
  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");
  39         }
  40       }
  41     }
  42     return booleanType;
  43   }
  44 };
  45
  46 class IteTypeRule {
  47   public:
  48   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  49       throw (TypeCheckingExceptionPrivate) {
  50     TypeNode iteType = n[1].getType(check);
  51     if( check ) {
  52       TypeNode booleanType = nodeManager->booleanType();
  53       if (n[0].getType(check) != booleanType) {
  54         throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
  55       }
  56       if (iteType != n[2].getType(check)) {
  57         throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type");
  58       }
  59     }
  60     return iteType;
  61   }
  62 };
  63
  64 } // boolean namespace
  65 } // theory namespace
  66 } // CVC4 namespace
  67
  68 #endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H_ */