src/theory/arrays/theory_arrays_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_arrays_type_rules.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: cconway
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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 Typing and cardinality rules for the theory of arrays
  15  **
  16  ** Typing and cardinality rules for the theory of arrays.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
  22 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace arrays {
  27
  28 struct ArraySelectTypeRule {
  29   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  30     throw (TypeCheckingExceptionPrivate, AssertionException) {
  31     Assert(n.getKind() == kind::SELECT);
  32     TypeNode arrayType = n[0].getType(check);
  33     if( check ) {
  34       if(!arrayType.isArray()) {
  35         throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
  36       }
  37       TypeNode indexType = n[1].getType(check);
  38       if(arrayType.getArrayIndexType() != indexType) {
  39         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
  40       }
  41     }
  42     return arrayType.getArrayConstituentType();
  43   }
  44 };/* struct ArraySelectTypeRule */
  45
  46 struct ArrayStoreTypeRule {
  47   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  48     throw (TypeCheckingExceptionPrivate, AssertionException) {
  49     Assert(n.getKind() == kind::STORE);
  50     TypeNode arrayType = n[0].getType(check);
  51     if( check ) {
  52       if(!arrayType.isArray()) {
  53         throw TypeCheckingExceptionPrivate(n, "array store operating on non-array");
  54       }
  55       TypeNode indexType = n[1].getType(check);
  56       TypeNode valueType = n[2].getType(check);
  57       if(arrayType.getArrayIndexType() != indexType) {
  58         throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
  59       }
  60       if(arrayType.getArrayConstituentType() != valueType) {
  61         throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
  62       }
  63     }
  64     return arrayType;
  65   }
  66 };/* struct ArrayStoreTypeRule */
  67
  68 struct ArrayTableFunTypeRule {
  69   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  70     throw (TypeCheckingExceptionPrivate, AssertionException) {
  71     Assert(n.getKind() == kind::ARR_TABLE_FUN);
  72     TypeNode arrayType = n[0].getType(check);
  73     if( check ) {
  74       if(!arrayType.isArray()) {
  75         throw TypeCheckingExceptionPrivate(n, "array table fun arg 0 is non-array");
  76       }
  77       TypeNode arrType2 = n[1].getType(check);
  78       if(!arrayType.isArray()) {
  79         throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
  80       }
  81       TypeNode indexType = n[2].getType(check);
  82       if(arrayType.getArrayIndexType() != indexType) {
  83         throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
  84       }
  85       indexType = n[3].getType(check);
  86       if(arrayType.getArrayIndexType() != indexType) {
  87         throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
  88       }
  89     }
  90     return arrayType.getArrayIndexType();
  91   }
  92 };/* struct ArrayStoreTypeRule */
  93
  94 struct CardinalityComputer {
  95   inline static Cardinality computeCardinality(TypeNode type) {
  96     Assert(type.getKind() == kind::ARRAY_TYPE);
  97
  98     Cardinality indexCard = type[0].getCardinality();
  99     Cardinality valueCard = type[1].getCardinality();
 100
 101     return valueCard ^ indexCard;
 102   }
 103 };/* struct CardinalityComputer */
 104
 105 }/* CVC4::theory::arrays namespace */
 106 }/* CVC4::theory namespace */
 107 }/* CVC4 namespace */
 108
 109 #endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */