1 /********************* */
2 /*! \file theory_arrays_type_rules.h
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
14 ** \brief Typing and cardinality rules for the theory of arrays
16 ** Typing and cardinality rules for the theory of arrays.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
22 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
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
);
34 if(!arrayType
.isArray()) {
35 throw TypeCheckingExceptionPrivate(n
, "array select operating on non-array");
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");
42 return arrayType
.getArrayConstituentType();
44 };/* struct ArraySelectTypeRule */
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
);
52 if(!arrayType
.isArray()) {
53 throw TypeCheckingExceptionPrivate(n
, "array store operating on non-array");
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");
60 if(arrayType
.getArrayConstituentType() != valueType
) {
61 throw TypeCheckingExceptionPrivate(n
, "array store not assigned with correct type for array");
66 };/* struct ArrayStoreTypeRule */
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
);
74 if(!arrayType
.isArray()) {
75 throw TypeCheckingExceptionPrivate(n
, "array table fun arg 0 is non-array");
77 TypeNode arrType2
= n
[1].getType(check
);
78 if(!arrayType
.isArray()) {
79 throw TypeCheckingExceptionPrivate(n
, "array table fun arg 1 is non-array");
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");
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");
90 return arrayType
.getArrayIndexType();
92 };/* struct ArrayStoreTypeRule */
94 struct CardinalityComputer
{
95 inline static Cardinality
computeCardinality(TypeNode type
) {
96 Assert(type
.getKind() == kind::ARRAY_TYPE
);
98 Cardinality indexCard
= type
[0].getCardinality();
99 Cardinality valueCard
= type
[1].getCardinality();
101 return valueCard
^ indexCard
;
103 };/* struct CardinalityComputer */
105 }/* CVC4::theory::arrays namespace */
106 }/* CVC4::theory namespace */
107 }/* CVC4 namespace */
109 #endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */