diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:54:33 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:54:33 +0000 |
commit | 2564d8730f768a8305325d4b6cc08211d8a3281d (patch) | |
tree | 56abf63023e3ffdadde2e7747dd2db7661962664 /src/theory/arrays | |
parent | 62ec86743289b26241d69b1701d4b3f547ee2bed (diff) |
Adding optional 'check' parameter to getType() methods
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 0eb88d800..5d0713a89 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -26,30 +26,34 @@ namespace theory { namespace arrays { struct ArraySelectTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::SELECT); - TypeNode arrayType = n[0].getType(); - TypeNode indexType = n[1].getType(); - if(arrayType.getArrayIndexType() != indexType) { - throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); + TypeNode arrayType = n[0].getType(check); + if( check ) { + TypeNode indexType = n[1].getType(check); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); + } } return arrayType.getArrayConstituentType(); } };/* struct ArraySelectTypeRule */ struct ArrayStoreTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::STORE); - TypeNode arrayType = n[0].getType(); - TypeNode indexType = n[1].getType(); - TypeNode valueType = n[2].getType(); - if(arrayType.getArrayIndexType() != indexType) { - throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); - } - if(arrayType.getArrayConstituentType() != valueType) { - throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); + TypeNode arrayType = n[0].getType(check); + if( check ) { + TypeNode indexType = n[1].getType(check); + TypeNode valueType = n[2].getType(check); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); + } + if(arrayType.getArrayConstituentType() != valueType) { + throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); + } } return arrayType; } |