src/theory/arith/theory_arith_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_arith_type_rules.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Tim King, Christopher L. Conway, Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 #include "util/subrange_bound.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace arith {
  27
  28
  29 class ArithConstantTypeRule {
  30 public:
  31   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  32       throw (TypeCheckingExceptionPrivate, AssertionException) {
  33     Assert(n.getKind() == kind::CONST_RATIONAL);
  34     if(n.getConst<Rational>().isIntegral()){
  35       return nodeManager->integerType();
  36     }else{
  37       return nodeManager->realType();
  38     }
  39   }
  40 };/* class ArithConstantTypeRule */
  41
  42 class ArithOperatorTypeRule {
  43 public:
  44   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  45       throw (TypeCheckingExceptionPrivate, AssertionException) {
  46     TypeNode integerType = nodeManager->integerType();
  47     TypeNode realType = nodeManager->realType();
  48     TNode::iterator child_it = n.begin();
  49     TNode::iterator child_it_end = n.end();
  50     bool isInteger = true;
  51     for(; child_it != child_it_end; ++child_it) {
  52       TypeNode childType = (*child_it).getType(check);
  53       if (!childType.isInteger()) {
  54         isInteger = false;
  55         if( !check ) { // if we're not checking, nothing left to do
  56           break;
  57         }
  58       }
  59       if( check ) {
  60         if(!childType.isReal()) {
  61           throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
  62         }
  63       }
  64     }
  65     switch(Kind k = n.getKind()) {
  66       case kind::TO_REAL:
  67         return realType;
  68       case kind::TO_INTEGER:
  69         return integerType;
  70       default: {
  71         bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
  72         return (isInteger && !isDivision ? integerType : realType);
  73       }
  74     }
  75   }
  76 };/* class ArithOperatorTypeRule */
  77
  78 class IntOperatorTypeRule {
  79 public:
  80   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  81       throw (TypeCheckingExceptionPrivate, AssertionException) {
  82     TNode::iterator child_it = n.begin();
  83     TNode::iterator child_it_end = n.end();
  84     if(check) {
  85       for(; child_it != child_it_end; ++child_it) {
  86         TypeNode childType = (*child_it).getType(check);
  87         if (!childType.isInteger()) {
  88           throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
  89         }
  90       }
  91     }
  92     return nodeManager->integerType();
  93   }
  94 };/* class IntOperatorTypeRule */
  95
  96 class ArithPredicateTypeRule {
  97 public:
  98   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  99       throw (TypeCheckingExceptionPrivate, AssertionException) {
 100     if( check ) {
 101       TypeNode lhsType = n[0].getType(check);
 102       if (!lhsType.isReal()) {
 103         Message() << lhsType << " : " << n[0] << std::endl;
 104         throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
 105       }
 106       TypeNode rhsType = n[1].getType(check);
 107       if (!rhsType.isReal()) {
 108         throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
 109       }
 110     }
 111     return nodeManager->booleanType();
 112   }
 113 };/* class ArithPredicateTypeRule */
 114
 115 class ArithUnaryPredicateTypeRule {
 116 public:
 117   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 118       throw (TypeCheckingExceptionPrivate, AssertionException) {
 119     if( check ) {
 120       TypeNode t = n[0].getType(check);
 121       if (!t.isReal()) {
 122         throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term");
 123       }
 124     }
 125     return nodeManager->booleanType();
 126   }
 127 };/* class ArithUnaryPredicateTypeRule */
 128
 129 class IntUnaryPredicateTypeRule {
 130 public:
 131   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 132       throw (TypeCheckingExceptionPrivate, AssertionException) {
 133     if( check ) {
 134       TypeNode t = n[0].getType(check);
 135       if (!t.isInteger()) {
 136         throw TypeCheckingExceptionPrivate(n, "expecting an integer term");
 137       }
 138     }
 139     return nodeManager->booleanType();
 140   }
 141 };/* class IntUnaryPredicateTypeRule */
 142
 143 class SubrangeProperties {
 144 public:
 145   inline static Cardinality computeCardinality(TypeNode type) {
 146     Assert(type.getKind() == kind::SUBRANGE_TYPE);
 147
 148     const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
 149     if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
 150       return Cardinality::INTEGERS;
 151     }
 152     return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
 153   }
 154
 155   inline static Node mkGroundTerm(TypeNode type) {
 156     Assert(type.getKind() == kind::SUBRANGE_TYPE);
 157
 158     const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
 159     if(bounds.lower.hasBound()) {
 160       return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
 161     }
 162     if(bounds.upper.hasBound()) {
 163       return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
 164     }
 165     return NodeManager::currentNM()->mkConst(Rational(0));
 166   }
 167 };/* class SubrangeProperties */
 168
 169 }/* CVC4::theory::arith namespace */
 170 }/* CVC4::theory namespace */
 171 }/* CVC4 namespace */
 172
 173 #endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */